isMax_iff — Mathlib

English

If i is a top element, then for any j, IsMax(j) holds iff j = i.

Русский

Пусть i — верхний элемент. Тогда для любого j верно: j максимален тогда и только тогда, когда j = i.

LaTeX

$$$\\\\mathrm{IsTop}(i) \\\\rightarrow (\\\\mathrm{IsMax}(j) \\\\leftrightarrow j = i)$$$

Lean4

theorem isMax_iff {α} [PartialOrder α] {i j : α} (h : IsTop i) : IsMax j ↔ j = i :=
  by
  simp_rw [le_antisymm_iff, h j, true_and]
  exact ⟨(· (h j)), Function.swap (fun _ ↦ h · |>.trans ·)⟩

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