isTrans — Mathlib

English

If x is an ordinal, then the membership relation restricted to elements of x is transitive: if a ∈ b and b ∈ c with a,b,c ∈ x, then a ∈ c.

Русский

Если x — ординал, то отношение членства между элементами x транзитивно: если a ∈ b и b ∈ c и a,b,c ∈ x, то a ∈ c.

LaTeX

$$$IsTrans\_\{ Subrel(\in, \in x)\}(a,b,c) \\text{ holds when } a,b,c \in x \\text{ and } a \in b \text{ and } b \in c \\Rightarrow a \in c$$$

Lean4

protected theorem isTrans (h : x.IsOrdinal) : IsTrans _ (Subrel (· ∈ ·) (· ∈ x)) :=
  ⟨fun _ _ c hab hbc => h.mem_trans' hab hbc c.2⟩

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