map_inf_principal_preimage — Mathlib

English

For f : α → β, l : Filter α, s : Set β, the pushforward of l ∧ 𝓟 (f⁻¹(s)) equals map(f, l) ∧ 𝓟 (s).

Русский

Для функции f: α → β, фильтра l на α и множества s ⊆ β, образ через f от l ∧ 𝓟(f⁻¹(s)) равен map(f, l) ∧ 𝓟(s).

LaTeX

$$$ \\operatorname{map} f (l \\land \\mathcal{P}(f^{-1}(s))) = \\operatorname{map} f l \\land \\mathcal{P}(s) $$$

Lean4

@[simp]
theorem map_inf_principal_preimage {f : α → β} {s : Set β} {l : Filter α} : map f (l ⊓ 𝓟 (f ⁻¹' s)) = map f l ⊓ 𝓟 s :=
  Filter.ext fun t => by simp only [mem_map', mem_inf_principal, mem_setOf_eq, mem_preimage]

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