Theorems · Theorem · general topology

Filter.map_comm

∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {φ : α → β} {θ : α → γ} {ψ : β → δ} {ρ : γ → δ},
  ψ ∘ φ = ρ ∘ θ → ∀ (F : Filter α), Filter.map ψ (Filter.map φ F) = Filter.map ρ (Filter.map θ F)

Defined in

Mathlib.Order.Filter.Map

Cited by

2 results in Mathlib

Foundations

Depth 13 from the axioms · uses Quot.sound