typein_le_typein' — Mathlib

English

For any ordinal o and x,y ∈ o.toType, typein x ≤ typein y iff x ≤ y.

Русский

Для любого ординала o и x,y ∈ o.toType, typein x ≤ typein y тогда и только тогда, когда x ≤ y.

LaTeX

$$$x \le y \iff \operatorname{typein} x \le \operatorname{typein} y$$$

Lean4

theorem typein_le_typein' (o : Ordinal) {x y : o.toType} :
    typein (α := o.toType) (· < ·) x ≤ typein (α := o.toType) (· < ·) y ↔ x ≤ y := by simp

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