isMin_iff — Mathlib

English

If i is a bottom element, then j is minimal iff j = i.

Русский

Если i является нижним элементом, то j минимален тогда и только тогда, когда j = i.

LaTeX

$$$\\\\mathrm{IsBot}(i) \\\\rightarrow (\\\\mathrm{IsMin}(j) \\\\leftrightarrow j = i)$$$

Lean4

theorem isMin_iff {α} [PartialOrder α] {i j : α} (h : IsBot i) : IsMin j ↔ j = i :=
  by
  simp_rw [le_antisymm_iff, h j, and_true]
  exact ⟨fun a ↦ a (h j), fun a h' ↦ fun _ ↦ Preorder.le_trans j i h' a (h h')⟩

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