orderBornology_isBounded — Mathlib

English

In a lattice with a bornology, IsBounded is equivalent to being bounded below and above.

Русский

В решётке с борологией ограниченность эквивалентна существованию нижней и верхней границы.

LaTeX

$$$\operatorname{IsBounded}(s) \iff (\operatorname{BddBelow}(s) \land \operatorname{BddAbove}(s))$$$

Lean4

@[simp]
theorem orderBornology_isBounded : orderBornology.IsBounded s ↔ BddBelow s ∧ BddAbove s := by
  simp [IsBounded, IsCobounded, -isCobounded_compl_iff]

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