Theorems · Theorem · general topology
ContinuousMap.sup_mem_subalgebra_closure
∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : CompactSpace X] (A : Subalgebra ℝ C(X, ℝ)) (f g : ↥A),
↑f ⊔ ↑g ∈ A.topologicalClosure- Cited by
- 1 results in Mathlib
- Foundations
- Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- TopologicalSpaceCompactSpace
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.
- Realstatement and proof · cited by 25,697
- TopologicalSpacestatement and proof · cited by 24,529
- ContinuousMapstatement and proof · cited by 2,491
- absproof · cited by 1,814
- Subalgebrastatement and proof · cited by 1,353
- CompactSpacestatement and proof · cited by 593
- Subalgebra.topologicalClosurestatement and proof · cited by 26
- Subalgebra.smul_memproof · cited by 20
- Subalgebra.add_memproof · cited by 19
- Subalgebra.le_topologicalClosureproof · cited by 4
- ContinuousMap.abs_mem_subalgebra_closureproof · cited by 2
- sup_eq_half_smul_add_add_abs_sub'proof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- ContinuousMap.sup_mem_closed_subalgebraproof · cited by 1