forall_generateFrom_mem_iff_mem_iff

English

For all x,y in α, the condition that all s satisfy (x ∈ s ↔ y ∈ s) for generates from S is equivalent to that condition holding for all s ∈ S.

Русский

Для любых x,y в α условие, что для всех s верно (x ∈ s ↔ y ∈ s) при порождении от S, эквивалентно условию для всех s ∈ S.

LaTeX

$$$(\\forall s, MeasurableSet[generateFrom S] s \\rightarrow (x \\in s \\leftrightarrow y \\in s)) \\iff (\\forall s \\in S, x \\in s \\leftrightarrow y \\in s)$$$

Lean4

theorem forall_generateFrom_mem_iff_mem_iff {S : Set (Set α)} {x y : α} :
    (∀ s, MeasurableSet[generateFrom S] s → (x ∈ s ↔ y ∈ s)) ↔ (∀ s ∈ S, x ∈ s ↔ y ∈ s) :=
  by
  refine ⟨fun H s hs ↦ H s (.basic s hs), fun H s ↦ ?_⟩
  apply generateFrom_induction
  · exact fun s hs _ ↦ H s hs
  · rfl
  · exact fun _ _ ↦ Iff.not
  · intro f _ hf
    simp only [mem_iUnion, hf]

Похожие утверждения