upperBounds_insert — Mathlib

English

In any preorder, the upper bounds of the union s ∪ {a} equal the intersection of the upper bounds of s with the interval [a, ∞).

Русский

Для любой предпорядочной структуры верхние границы множества s ∪ {a} равны пересечению верхних границ s с интервалом [a, ∞).

LaTeX

$$$\operatorname{upperBounds}(s \\cup \\{a\\}) = \operatorname{Icc?}([a, \\infty)) \cap \operatorname{upperBounds}(s)$$$

Lean4

@[simp]
theorem upperBounds_insert (a : α) (s : Set α) : upperBounds (insert a s) = Ici a ∩ upperBounds s := by
  rw [insert_eq, upperBounds_union, upperBounds_singleton]

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