coe_le_coe — Mathlib

English

For any a,b ∈ Regular α, the embedding is order-preserving: (a:α) ≤ b iff a ≤ b in Regular α.

Русский

Для любых a,b ∈ Regular α вложение сохраняет порядок: (a:α) ≤ b тогда и только если a ≤ b в Regular α.

LaTeX

$$$\forall a,b \in \mathrm{Regular}(\alpha),\ (a : \alpha) \le b \iff a \le b.$$$

Lean4

@[simp, norm_cast]
theorem coe_le_coe {a b : Regular α} : (a : α) ≤ b ↔ a ≤ b :=
  Iff.rfl

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