Structures · Topology
FirstCountableTopology
A first-countable space is one in which every point has a countable neighborhood basis.
- Defined in
- Mathlib.Topology.Bases
- Shape
- One type argument · adds nhds_generated_countable
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances7
- DomMulAct
- DomAddAct
- SchwartzMap
- Prod
- OrderDual
- Set.Elem
- HasQuotient.Quotient
How is a type an instance?
Loading the hierarchy index…
Assumed by125
- exists_seq_strictAnti_tendsto
- exists_seq_strictAnti_tendsto'
- IsCompact.isSeqCompact
- exists_seq_strictMono_tendsto'
- MeasureTheory.IsStoppingTime.measurableSet_eq'
- MeasureTheory.IsStoppingTime.measurableSet_eq
- eventually_le_limsup
- ae_le_essSup
- IsCompact.tendsto_subseq
- MeasureTheory.ae_const_le_iff_forall_lt_measure_zero
- MeasureTheory.continuousAt_setToFun_of_dominated
- MeasureTheory.IsStoppingTime.measurableSet_ge
- MeasureTheory.continuousWithinAt_setToFun_of_dominated
- MeasureTheory.continuousAt_of_dominated
- Dense.exists_seq_strictMono_tendsto_of_lt
- exists_seq_strictMono_tendsto
- MeasureTheory.tendsto_measure_biInter_gt
- limsup_eq_bot
- MapClusterPt.exists_seq_tendsto
- MeasureTheory.IsStoppingTime.biInf
- MeasureTheory.Adapted.isStoppingTime_hittingBtwn_isStoppingTime
- MeasureTheory.IsStoppingTime.measurableSet_eq_le
- MeasureTheory.continuousOn_setToFun_of_dominated
- MeasureTheory.continuous_setToFun_of_dominated
- DenseRange.exists_seq_strictMono_tendsto
- BddAbove.continuous_convolution_right_of_integrable
- MeasureTheory.IsStoppingTime.measurableSet_lt
- MeasureTheory.memLp_stoppedProcess_of_mem_finset
- ClusterPt.exists_seq_tendsto
- Summable.countable_support
- Dense.exists_seq_strictMono_tendsto
- exists_seq_tendsto_sSup
- intervalIntegral.continuousAt_of_dominated_interval
- MeasureTheory.Martingale.stoppedValue_ae_eq_condExp_of_le_const_of_countable_range
- eventually_le_const_iff_forall_gt_eventually_lt_const
- MeasureTheory.continuous_of_dominated
- VectorFourier.fourierIntegral_continuous
- IsGδ.singleton
- DenseRange.exists_seq_strictMono_tendsto_of_lt
- exists_seq_tendsto_sInf
- meas_essSup_lt
- ProbabilityTheory.IsPreLocalizingSequence.isLocalizingSequence_biInf
- MeasureTheory.isStoppingTime_of_measurableSet_lt_of_isRightContinuous
- MeasureTheory.Martingale.stoppedValue_ae_eq_restrict_eq
- intervalIntegral.continuousWithinAt_of_dominated_interval
- MeasureTheory.integrable_stoppedProcess_of_mem_finset
- IsCountablyCompact.isSeqCompact
- MeasureTheory.Martingale.condExp_stopping_time_ae_eq_restrict_eq_const_of_le_const
- Topology.IsInducing.firstCountableTopology
- LinearMap.continuousAt_zero_of_locally_bounded
Ancestors0
No ancestors.