not_isMin — Mathlib

English

In a directed poset, if an element is maximal then it cannot be minimal.

Русский

В направленном частично упорядоченном множестве если элемент максимален, то он не может быть минимальным.

LaTeX

$$$\forall \{\beta\} [PartialOrder\ \beta] [Nontrivial\ \beta] [IsDirected \beta (\le )], \forall b:\beta, \ IsMax(b) \rightarrow \neg IsMin(b).$$$

Lean4

protected theorem not_isMin [IsDirected β (· ≤ ·)] {b : β} (hb : IsMax b) : ¬IsMin b := fun hb' ↦
  hb.toDual.not_isMax hb'.toDual

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