mem_trans

Mathlib.SetTheory.ZFC.Ordinal

URI: https://scilib.ai/kg/mathlib#ZFSet.IsOrdinal.mem_trans

English

If z is an ordinal and x ∈ y ∈ z, then x ∈ z.

Русский

Если z ординал и существует цепочка x ∈ y ∈ z, то x ∈ z.

LaTeX

$$$IsOrdinal(z) \Rightarrow x \in y \Rightarrow y \in z \Rightarrow x \in z$$$

Lean4

theorem mem_trans (h : z.IsOrdinal) : x ∈ y → y ∈ z → x ∈ z :=
  h.isTransitive.mem_trans

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru