union — Mathlib

English

If s =^l t and s' =^l t', then s ∪ s' =^l t ∪ t'.

Русский

Если s =^l t и s' =^l t', то s ∪ s' =^l t ∪ t'.

LaTeX

$$$\\\\forall l \\\\ (l : Filter \\\\alpha), \\\\forall s,t,s',t' \\\\subseteq α, \\\\ (s =^l t) \\\\Rightarrow \\\\ (s' =^l t') \\\\Rightarrow \\\\bigl(s \\\\cup s' =^l t \\\\cup t'\\\\bigr)$$$

Lean4

@[gcongr]
theorem union {s t s' t' : Set α} {l : Filter α} (h : s =ᶠ[l] t) (h' : s' =ᶠ[l] t') :
    (s ∪ s' : Set α) =ᶠ[l] (t ∪ t' : Set α) :=
  h.comp₂ (· ∨ ·) h'

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