bddAbove — Mathlib

English

A finite subset of a directed preordered nonempty type has an upper bound.

Русский

Конечное подмножество направленного порядка в ненулевом типе имеет верхнюю грань.

LaTeX

$$$s\text{ finite} \Rightarrow \exists u, \forall x\in s, x \le u.$$$

Lean4

/-- A finite set is bounded above. -/
protected theorem bddAbove (hs : s.Finite) : BddAbove s :=
  Finite.induction_on _ hs bddAbove_empty fun _ _ h => h.insert _

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