Theorems · Theorem · general topology

Ctop.Realizer.mk.injEq

∀ {α : Type u_6} [T : TopologicalSpace α] (σ : Type u_5) (F : Ctop α σ) (eq : F.toTopsp = T) (σ_1 : Type u_5)
  (F_1 : Ctop α σ_1) (eq_1 : F_1.toTopsp = T),
  ({ σ := σ, F := F, eq := eq } = { σ := σ_1, F := F_1, eq := eq_1 }) = (σ = σ_1 ∧ F ≍ F_1)

Defined in

Mathlib.Data.Analysis.Topology

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

TopologicalSpace