sUnion' — Mathlib

English

If every y ∈ x is transitive, then x.sUnion is transitive.

Русский

Если каждый элемент y множества x транзитивен, тогда x.sUnion транзитивен.

LaTeX

$$$ (\\forall y \\in x, y.IsTransitive) \\Rightarrow x.sUnion.IsTransitive. $$$

Lean4

/-- The union of transitive sets is transitive. -/
theorem sUnion' (H : ∀ y ∈ x, IsTransitive y) : (⋃₀ x : ZFSet).IsTransitive := fun y hy z hz =>
  by
  rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
  exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw

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