bddBelow_upperClosure — Mathlib

English

In a preorder, the set upperClosure(s) is bounded below iff s is bounded below.

Русский

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

LaTeX

$$$ \\operatorname{BddBelow}(\\operatorname{upperClosure}(s)) \\iff \\operatorname{BddBelow}(s) $$$

Lean4

@[simp]
theorem bddBelow_upperClosure : BddBelow (upperClosure s : Set α) ↔ BddBelow s := by
  simp_rw [BddBelow, lowerBounds_upperClosure]

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