map_const — Mathlib

English

If ψ ∘ φ = ρ ∘ θ, then map ψ (map φ F) = map ρ (map θ F) for any filter F.

Русский

Если ψ ∘ φ = ρ ∘ θ, тогда для любого фильтра F выполняется map ψ (map φ F) = map ρ (map θ F).

LaTeX

$$$ \text{map }\psi (\text{map }\phi F) = \text{map }\rho (\text{map }\theta F) \quad \text{whenever } \psi \circ \phi = \rho \circ \theta $$$

Lean4

theorem map_const [NeBot f] {c : β} : (f.map fun _ => c) = pure c :=
  by
  ext s
  by_cases h : c ∈ s <;> simp [h]

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