not_isMax' — Mathlib

English

In a directed partially ordered set, no element can be both minimal and maximal.

Русский

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

LaTeX

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

Lean4

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

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