Theorems · Theorem · general topology
Subalgebra.separatesPoints_monotone
∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_2} [inst_1 : CommSemiring R] {A : Type u_3}
[inst_2 : TopologicalSpace A] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : IsTopologicalSemiring A],
Monotone fun s => s.SeparatesPoints- Defined in
- Mathlib.Topology.ContinuousMap.Algebra
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- TopologicalSpacestatement and proof · cited by 24,529
- Semiringstatement and proof · cited by 13,802
- Algebrastatement and proof · cited by 11,388
- CommSemiringstatement and proof · cited by 10,911
- SetLike.coeproof · cited by 8,199
- Set.imageproof · cited by 5,609
- ContinuousMapstatement and proof · cited by 2,491
- Monotonestatement · cited by 1,397
- Subalgebrastatement and proof · cited by 1,353
- IsTopologicalSemiringstatement and proof · cited by 442
- Subalgebra.SeparatesPointsstatement and proof · cited by 18
Cited by2
Results whose statement or proof uses this declaration.
- polynomialFunctions.starClosure_topologicalClosureproof · cited by 4
- ContinuousMap.subalgebra_topologicalClosure_eq_top_of_separatesPointsproof · cited by 3