English
A set t is measurable in generateFrom {s} if and only if t equals ∅, s, sᶜ, or univ.
Русский
Множество t измеримо в generateFrom {s} тогда и только тогда, когда t равно ∅, s, sᶜ или унив.
LaTeX
$$$MeasurableSet[MeasurableSpace.generateFrom\\{ s \\}] t \\leftrightarrow t = \\emptyset \\lor t = s \\lor t = s^c \\lor t = univ$$$
Lean4
theorem measurableSet_generateFrom_singleton_iff {s t : Set α} :
MeasurableSet[MeasurableSpace.generateFrom { s }] t ↔ t = ∅ ∨ t = s ∨ t = sᶜ ∨ t = univ :=
by
simp_rw [MeasurableSpace.generateFrom_singleton]
unfold MeasurableSet MeasurableSpace.MeasurableSet' MeasurableSpace.comap
simp_rw [MeasurableSpace.measurableSet_top, true_and]
constructor
· rintro ⟨x, rfl⟩
by_cases hT : True ∈ x
· by_cases hF : False ∈ x
· refine Or.inr <| Or.inr <| Or.inr <| subset_antisymm (subset_univ _) ?_
suffices x = univ by simp only [this, preimage_univ, subset_refl]
refine subset_antisymm (subset_univ _) ?_
rw [univ_eq_true_false]
rintro - (rfl | rfl)
· assumption
· assumption
· have hx : x = { True } := by
ext p
refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hT⟩
by_contra hpneg
rw [eq_iff_iff, iff_true, ← false_iff] at hpneg
exact hF (by convert hp)
simp [hx]
· by_cases hF : False ∈ x
· have hx : x = { False } := by
ext p
refine ⟨fun hp ↦ mem_singleton_iff.2 ?_, fun hp ↦ hp ▸ hF⟩
grind
refine Or.inr <| Or.inr <| Or.inl <| ?_
simp [hx, compl_def]
· refine Or.inl <| subset_antisymm ?_ <| empty_subset _
suffices x ⊆ ∅ by
rw [subset_empty_iff] at this
simp only [this, preimage_empty, subset_refl]
intro p hp
fin_cases p
· contradiction
· contradiction
· rintro (rfl | rfl | rfl | rfl)
on_goal 1 => use ∅
on_goal 2 => use { True }
on_goal 3 => use { False }
on_goal 4 => use Set.univ
all_goals simp [compl_def]
