coheight_eq_coe_iff_maximal_le_coheight

English

The equality coheight a = n holds iff a is maximal among those with coheight at least n, i.e., a is the largest element with coheight at least n.

Русский

Ко-высота элемента a равна n тогда, когда a является максимальным среди элементов ко-высоты не ниже n.

LaTeX

$$$$ \operatorname{coheight}(a) = n \iff \operatorname{Maximal}\bigl( \lambda y, \; n \le \operatorname{coheight}(y) \bigr) a $$$$

Lean4

/-- The elements of finite coheight `n` are the maximal elements among those of coheight `≥ n`. -/
theorem coheight_eq_coe_iff_maximal_le_coheight {a : α} {n : ℕ} :
    coheight a = n ↔ Maximal (fun y => n ≤ coheight y) a :=
  height_eq_coe_iff_minimal_le_height (α := αᵒᵈ)

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