Theorems · Theorem · general topology

Filter.Realizer.mk.inj

∀ {α : Type u_1} {f : Filter α} {σ : Type u_5} {F : CFilter (Set α) σ} {eq : F.toFilter = f} {σ_1 : Type u_5}
  {F_1 : CFilter (Set α) σ_1} {eq_1 : F_1.toFilter = f},
  { σ := σ, F := F, eq := eq } = { σ := σ_1, F := F_1, eq := eq_1 } → σ = σ_1 ∧ F ≍ F_1

Defined in

Mathlib.Data.Analysis.Filter

Cited by

1 results in Mathlib

Foundations

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