Theorems · Theorem · general topology

Ultrafilter.comap_comap

∀ {α : Type u} {β : Type v} {γ : Type u_1} (f : Ultrafilter γ) {m : α → β} {n : β → γ} (inj₀ : Function.Injective n)
  (large₀ : Set.range n ∈ f) (inj₁ : Function.Injective m) (large₁ : Set.range m ∈ f.comap inj₀ large₀)
  (inj₂ : optParam (Function.Injective (n ∘ m)) ⋯) (large₂ : optParam (Set.range (n ∘ m) ∈ f) ⋯),
  (f.comap inj₀ large₀).comap inj₁ large₁ = f.comap inj₂ large₂

Defined in

Mathlib.Order.Filter.Ultrafilter.Defs

Cited by

0 results in Mathlib

Foundations

Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound