sUnion — Mathlib

English

The union of a transitive set is transitive.

Русский

Объединение транзитивного множества является транзитивным.

LaTeX

$$$ \\forall x, x.IsTransitive \\Rightarrow (\\bigcup_{0} x).IsTransitive. $$$

Lean4

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

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