Source indexedlemma · leanprover/lean4:v4.32.0

measurableSet_E

Carleson.TileStructure · Carleson/TileStructure.lean:139 to 146

Mathematical statement

Exact Lean statement

lemma measurableSet_E {p : 𝔓 X} : MeasurableSet (E p)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma measurableSet_E {p : 𝔓 X} : MeasurableSet (E p) := by  refine (Measurable.and ?_ (Measurable.and ?_ ?_)).setOf  · rw [← measurableSet_setOf]; exact coeGrid_measurable  · simp_rw [← mem_preimage, ← measurableSet_setOf]; exact SimpleFunc.measurableSet_preimage ..  · apply (measurable_set_mem _).comp    apply Measurable.comp (f := fun x ↦ (σ₁ x, σ₂ x)) (g := fun p ↦ Icc p.1 p.2)    · exact measurable_from_prod_countable_left fun _ _ _ ↦ trivial    · exact measurable_σ₁.prodMk measurable_σ₂