mem — Mathlib

English

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

Русский

Если x — ординал и y ∈ x, то y — ординал.

LaTeX

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

Lean4

protected theorem mem (hx : x.IsOrdinal) (hy : y ∈ x) : y.IsOrdinal :=
  have := hx.isTrans
  let f : _ ↪r Subrel (· ∈ ·) (· ∈ x) := Subrel.inclusionEmbedding (· ∈ ·) (hx.subset_of_mem hy)
  isOrdinal_iff_isTrans.2 ⟨fun _ hz _ ha ↦ hx.mem_trans' ha hz hy, f.isTrans⟩

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