coheight_le_coheight — Mathlib

English

Let α be a preorder. For all a,b ∈ α, if b ≤ a, then coheight(a) ≤ coheight(b).

Русский

Пусть α — частично упорядоченное множество. Для любых a, b ∈ α, если b ≤ a, то coheight(a) ≤ coheight(b).

LaTeX

$$$\forall a,b \in \alpha,\ b \le a \Rightarrow \operatorname{coheight}(a) \le \operatorname{coheight}(b)$$$

Lean4

@[gcongr]
protected theorem _root_.GCongr.coheight_le_coheight (a b : α) (hba : b ≤ a) : coheight a ≤ coheight b :=
  coheight_anti hba

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