isTransitive_iff_mem_trans — Mathlib

English

A set z is transitive iff ∀ x,y with x ∈ y and y ∈ z, we have x ∈ z.

Русский

Множество z транзитивно тогда и только тогда, когда для любых x,y с x ∈ y и y ∈ z выполняется x ∈ z.

LaTeX

$$$ z.IsTransitive \\iff \\forall x,y, x \\in y \\to y \\in z \\to x \\in z. $$$

Lean4

theorem isTransitive_iff_mem_trans : z.IsTransitive ↔ ∀ {x y : ZFSet}, x ∈ y → y ∈ z → x ∈ z :=
  ⟨fun h _ _ hx hy => h.subset_of_mem hy hx, fun H _ hx _ hy => H hy hx⟩

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