not_isMax — Mathlib

English

In a directed setting, a minimal element cannot be maximal.

Русский

В направленной системе минимальный элемент не может быть максимальным.

LaTeX

$$$IsMin(b) \rightarrow \lnot IsMax(b)$$$

Lean4

protected theorem not_isMax [IsDirected β (· ≥ ·)] {b : β} (hb : IsMin b) : ¬IsMax b :=
  by
  intro hb'
  obtain ⟨a, c, hac⟩ := exists_lt_of_directed_ge β
  have := hb.isBot a
  obtain rfl := (hb' <| this).antisymm this
  exact hb'.not_lt hac

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