union — Mathlib

English

If s and t are IsRelUpperSet for P, then s ∪ t is IsRelUpperSet for P.

Русский

Если s и t — IsRelUpperSet для P, тогда s ∪ t — IsRelUpperSet для P.

LaTeX

$$$IsRelUpperSet\\;s\\;P \\rightarrow IsRelUpperSet\\;t\\;P \\rightarrow IsRelUpperSet\\; (s \\cup t) \\;P$$$

Lean4

theorem union (hs : IsRelUpperSet s P) (ht : IsRelUpperSet t P) : IsRelUpperSet (s ∪ t) P := fun b mb ↦ by
  cases mb with
  | inl h => exact ⟨(hs h).1, fun _ x y ↦ .inl ((hs h).2 x y)⟩
  | inr h => exact ⟨(ht h).1, fun _ x y ↦ .inr ((ht h).2 x y)⟩

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