lift'_inf — Mathlib

English

If s respects intersections, then (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s.

Русский

Если s сохраняет пересечения, то (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s.

LaTeX

$$$(f \\inf g).lift'\\, s = f.lift'\\, s \\inf g.lift'\\, s$$$

Lean4

theorem lift'_inf (f g : Filter α) {s : Set α → Set β} (hs : ∀ t₁ t₂, s (t₁ ∩ t₂) = s t₁ ∩ s t₂) :
    (f ⊓ g).lift' s = f.lift' s ⊓ g.lift' s :=
  by
  rw [inf_eq_iInf, inf_eq_iInf, lift'_iInf hs]
  refine iInf_congr ?_
  rintro (_ | _) <;> rfl

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