lowerBounds_insert — Mathlib

English

In any preorder, the lower bounds of s ∪ {a} equal the intersection of the lower bounds of s with the interval (-∞, a].

Русский

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

LaTeX

$$$\operatorname{lowerBounds}(s \\cup \\{a\\}) = Iic(a) \cap \operatorname{lowerBounds}(s)$$$

Lean4

@[simp]
theorem lowerBounds_insert (a : α) (s : Set α) : lowerBounds (insert a s) = Iic a ∩ lowerBounds s := by
  rw [insert_eq, lowerBounds_union, lowerBounds_singleton]

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