union — Mathlib

English

If two subsets s and t are complete, then their union s ∪ t is also complete.

Русский

Если два подмножества s и t полно, то их объединение s ∪ t тоже полно.

LaTeX

$$$IsComplete(s) \\to IsComplete(t) \\to IsComplete(s \\cup t)$$$

Lean4

protected theorem union {s t : Set α} (hs : IsComplete s) (ht : IsComplete t) : IsComplete (s ∪ t) :=
  by
  simp only [isComplete_iff_ultrafilter', Ultrafilter.union_mem_iff, or_imp] at *
  exact fun l hl =>
    ⟨fun hsl => (hs l hl hsl).imp fun x hx => ⟨Or.inl hx.1, hx.2⟩, fun htl =>
      (ht l hl htl).imp fun x hx => ⟨Or.inr hx.1, hx.2⟩⟩

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