inter — 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 \\cap s' =^l t \\cap t'\\\\bigr)$$$

Lean4

@[gcongr]
theorem inter {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'

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