not_lt_minimum_of_mem' — Mathlib

English

For any a ∈ l, the with-top minimum is not strictly greater than a.

Русский

Для любого a ∈ l нижний максимум не больше a; в точности, a не меньше минимума.

LaTeX

$$$\forall ha.\; ha \in l \rightarrow \Not ( (a : \mathrm{WithTop}\; \alpha) < \operatorname{minimum} l )$$$

Lean4

theorem not_lt_minimum_of_mem' (ha : a ∈ l) : ¬(a : WithTop α) < minimum l := by
  cases h : l.minimum <;> simp_all [not_lt_minimum_of_mem ha]

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