isTransitive_iff_sUnion_subset — Mathlib

English

A set x is transitive iff ⋃₀ x ⊆ x.

Русский

Множество x транзитивно тогда и только тогда, когда ⋃₀ x ⊆ x.

LaTeX

$$$ x.IsTransitive \\iff (\\bigcup_{0} x \\subseteq x). $$$

Lean4

theorem isTransitive_iff_sUnion_subset : x.IsTransitive ↔ (⋃₀ x : ZFSet) ⊆ x :=
  by
  constructor <;> intro h y hy
  · obtain ⟨z, hz, hz'⟩ := mem_sUnion.1 hy
    exact h.mem_trans hz' hz
  · exact fun z hz ↦ h <| mem_sUnion_of_mem hz hy

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