upperBounds_union — Mathlib

English

In a preorder, the upper bounds of s ∪ t are exactly the intersection of upper bounds of s and upper bounds of t.

Русский

В предореуденном множество верхние границы s ∪ t равны пересечению верхних границ s и верхних границ t.

LaTeX

$$$\\mathrm{upperBounds}(s \\cup t) = \\mathrm{upperBounds}(s) \\cap \\mathrm{upperBounds}(t)$$$

Lean4

@[simp]
theorem upperBounds_union : upperBounds (s ∪ t) = upperBounds s ∩ upperBounds t :=
  Subset.antisymm (fun _ hb => ⟨fun _ hx => hb (Or.inl hx), fun _ hx => hb (Or.inr hx)⟩) fun _ hb _ hx =>
    hx.elim (fun hs => hb.1 hs) fun ht => hb.2 ht

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