Theorems · Theorem · general topology

DiscreteQuotient.exists_of_compat

∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] (Qs : (Q : DiscreteQuotient X) → Quotient Q.toSetoid),
  (∀ (A B : DiscreteQuotient X) (h : A ≤ B), DiscreteQuotient.ofLE h (Qs A) = Qs B) →
    ∃ x, ∀ (Q : DiscreteQuotient X), Q.proj x = Qs Q

Defined in: Mathlib.Topology.DiscreteQuotient
Cited by: 0 results in Mathlib
Foundations: Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace CompactSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites17

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

TopologicalSpacestatement and proof · cited by 24,529
Set.preimageproof · cited by 4,946
Set.iInterproof · cited by 1,084
CompactSpacestatement and proof · cited by 593
Set.mem_iInterproof · cited by 69
DiscreteQuotientstatement and proof · cited by 65
DiscreteQuotient.toSetoidstatement and proof · cited by 45
IsClosed.isCompactproof · cited by 43
Set.singleton_nonemptyproof · cited by 32
DiscreteQuotient.projstatement and proof · cited by 23
DiscreteQuotient.ofLEstatement and proof · cited by 14
IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosedproof · cited by 11

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.