Structures · Analysis
HasOuterApproxClosed
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.
- Shape
- One type argument · adds exAppr
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by68
- IsClosed.apprSeq
- Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction
- indicator_indepFun_pi_of_prod_bcf
- HasOuterApproxClosed.exAppr
- HasOuterApproxClosed.apprSeq_apply_le_one
- MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto
- indepFun_pi_of_prod_bcf
- MeasureTheory.ProbabilityMeasure.le_liminf_measure_open_of_tendsto
- Measure.ext_of_integral_prod_mul_boundedContinuousFunction
- MeasureTheory.FiniteMeasure.ext_of_forall_lintegral_eq
- pi_indepFun_of_prod_bcf
- HasOuterApproxClosed.tendsto_lintegral_apprSeq
- Measure.ext_of_integral_mul_prod_boundedContinuousFunction
- HasOuterApproxClosed.tendsto_apprSeq
- MeasureTheory.ext_of_forall_lintegral_eq_of_IsFiniteMeasure
- indicator_indepFun_pi_of_bcf
- pi_indepFun_pi_of_prod_bcf
- HasOuterApproxClosed.apprSeq_apply_eq_one
- Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction
- indepFun_pi_of_bcf
- Measure.eq_prod_of_integral_mul_prod_boundedContinuousFunction
- indicator_indepFun_process_of_prod_bcf
- indepSets_comap_pi_of_prod_bcf
- indepSets_comap_pi_of_bcf
- indepSets_comap_of_bcf
- indepSets_comap_process_of_prod_bcf
- MeasureTheory.ext_of_forall_integral_eq_of_IsFiniteMeasure
- Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction
- Measure.ext_of_integral_mul_prod_boundedContinuousFunction'
- indicator_indepFun_of_bcf
- MeasureTheory.ProbabilityMeasure.tendsto_measure_of_null_frontier_of_tendsto'
- Measure.ext_of_integral_prod_mul_boundedContinuousFunction'
- MeasureTheory.FiniteMeasure.limsup_measure_closed_le_of_tendsto
- indicator_indepFun_process_of_bcf
- pi_indepFun_of_bcf
- indepSets_comap_process_of_bcf
- Measure.ext_of_lintegral_prod_mul_prod_boundedContinuousFunction
- MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure
- MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN
- Measure.ext_of_integral_mul_boundedContinuousFunction
- Measure.eq_prod_of_integral_mul_boundedContinuousFunction
- Measure.ext_of_integral_prod_mul_prod_boundedContinuousFunction'
- HasOuterApproxClosed.measure_le_lintegral
- MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto
- pi_indepFun_pi_of_bcf
- MeasureTheory.ProbabilityMeasure.t2Space
- MeasureTheory.FiniteMeasure.t2Space
- Measure.eq_prod_of_integral_prod_mul_prod_boundedContinuousFunction'
- MeasureTheory.FiniteMeasure.ext_of_forall_integral_eq
- MeasureTheory.FiniteMeasure.isEmbedding_toWeakDualBCNN
Ancestors0
No ancestors.