Theorems · Inductive type · measure theory
HasOuterApproxClosed
(X : Type u_1) → [TopologicalSpace X] → Prop
A type class for topological spaces in which the indicator functions of closed sets can be approximated pointwise from above by a sequence of bounded continuous functions.
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement · cited by 24,529
Cited by68
Results whose statement or proof uses this declaration.
- IsClosed.apprSeqstatement and proof · cited by 10
- indicator_indepFun_pi_of_prod_bcfstatement and proof · cited by 4
- Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunctionstatement and proof · cited by 4
- indepFun_pi_of_prod_bcfstatement and proof · cited by 3
- MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendstostatement and proof · cited by 3
- MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendstostatement and proof · cited by 3
- HasOuterApproxClosed.apprSeq_apply_le_onestatement and proof · cited by 3
- HasOuterApproxClosed.exApprstatement and proof · cited by 3
- Measure.ext_of_integral_prod_mul_boundedContinuousFunctionstatement and proof · cited by 3
- indicator_indepFun_pi_of_bcfstatement and proof · cited by 2
- MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasurestatement and proof · cited by 2
- MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eqstatement and proof · cited by 2