bddAbove_lowerClosure — Mathlib

English

In a preorder, the set obtained by taking all lower elements of the lower closure of s is bounded above iff s is bounded above.

Русский

В частично упорядоченном множестве множество, получаемое взятием всех меньших элементов нижнего замыкания s, ограничено сверху тогда и только тогда, когда s ограничено сверху.

LaTeX

$$$ \\operatorname{BddAbove}(\\operatorname{LowerClosure}(s)) \\iff \\operatorname{BddAbove}(s) $$$

Lean4

@[simp]
theorem bddAbove_lowerClosure : BddAbove (lowerClosure s : Set α) ↔ BddAbove s := by
  simp_rw [BddAbove, upperBounds_lowerClosure]

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