isMax_coe — Mathlib

English

For a flag element a in α, IsMax((a : α)) is equivalent to IsMax(a) in the flag.

Русский

Для элемента флага a ∈ s, свойство максимума сохраняется при включении через коэффициент: IsMax((a:α)) эквивалентно IsMax(a).

LaTeX

$$$ \\text{IsMax}(a: \\alpha) \\iff \\text{IsMax}(a). $$$

Lean4

@[simp]
theorem isMax_coe : IsMax (a : α) ↔ IsMax a where
  mp h b hab := h hab
  mpr h b
    hab := by
    refine @h ⟨b, mem_iff_forall_le_or_ge.2 fun c hc ↦ ?_⟩ hab
    classical exact .inr <| hab.trans' <| h.isTop ⟨c, hc⟩

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