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 \\cap t) \\;P$$$

Lean4

theorem union (hs : IsRelLowerSet s P) (ht : IsRelLowerSet t P) : IsRelLowerSet (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)⟩

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