Filter

📁 Source: Mathlib/Topology/Filter.lean

Statistics

Metric	Count
Definitions `instTopologicalSpace`	1
Theorems `nhds`, `nhds`, `nhds`, `nhds`, `nhds`, `nhds'`, `nhds`, `closure_singleton`, `continuous_nhds`, `instIsCountablyGeneratedNhds`, `instT0Space`, `isInducing_nhds`, `isOpen_Iic_principal`, `isOpen_iff`, `isOpen_setOf_mem`, `isTopologicalBasis_Iic_principal`, `mem_closure`, `mem_interior`, `mem_nhds_iff`, `mem_nhds_iff'`, `monotone_nhds`, `nhds_atBot`, `nhds_atTop`, `nhds_bot`, `nhds_eq`, `nhds_eq'`, `nhds_iInf`, `nhds_inf`, `nhds_mono`, `nhds_nhds`, `nhds_principal`, `nhds_pure`, `nhds_top`, `sInter_nhds`, `specializes_iff_le`, `tendsto_nhds`, `tendsto_nhds_atBot_iff`, `tendsto_nhds_atTop_iff`, `tendsto_pure_self`	39
Total	40

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds` 📖	mathematical	`Continuous`	`Filter` `Filter.instTopologicalSpace` `nhds`	—	`comp` `Filter.continuous_nhds`

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds` 📖	mathematical	`ContinuousAt`	`Filter` `Filter.instTopologicalSpace` `nhds`	—	`Filter.Tendsto.nhds`

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds` 📖	mathematical	`ContinuousOn`	`Filter` `Filter.instTopologicalSpace` `nhds`	—	`ContinuousWithinAt.nhds`

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds` 📖	mathematical	`ContinuousWithinAt`	`Filter` `Filter.instTopologicalSpace` `nhds`	—	`Filter.Tendsto.nhds`

Filter

Definitions

Name	Category	Theorems
`instTopologicalSpace` 📖	CompOp	44 math math: `tendsto_nhds_atBot_iff`, `nhds_atBot`, `nhds_eq'`, `isInducing_nhds`, `nhds_top`, `mem_nhds_iff`, `HasBasis.nhds`, `tendsto_nhds_atBot`, `tendsto_nhds`, `nhds_inf`, `mem_closure`, `nhds_bot`, `Continuous.nhds`, `nhds_eq`, `Tendsto.nhds`, `ContinuousWithinAt.nhds`, `Tendsto.nhds_atBot`, `mem_nhds_iff'`, `nhds_principal`, `isOpen_setOf_mem`, `nhds_pure`, `HasBasis.nhds'`, `closure_singleton`, `nhds_mono`, `mem_interior`, `tendsto_nhds_atTop_iff`, `nhds_iInf`, `isProperMap_iff_isClosedMap_filter`, `monotone_nhds`, `instIsCountablyGeneratedNhds`, `isTopologicalBasis_Iic_principal`, `ContinuousAt.nhds`, `instT0Space`, `nhds_nhds`, `tendsto_nhds_atTop`, `Tendsto.nhds_atTop`, `nhds_atTop`, `ContinuousOn.nhds`, `continuous_nhds`, `sInter_nhds`, `isOpen_iff`, `isOpen_Iic_principal`, `specializes_iff_le`, `tendsto_pure_self`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_singleton` 📖	mathematical	—	`closure` `Filter` `instTopologicalSpace` `Set` `Set.instSingletonSet` `Set.Ici` `PartialOrder.toPreorder` `instPartialOrder`	—	`Set.ext`
`continuous_nhds` 📖	mathematical	—	`Continuous` `Filter` `instTopologicalSpace` `nhds`	—	`Topology.IsInducing.continuous` `isInducing_nhds`
`instIsCountablyGeneratedNhds` 📖	mathematical	—	`IsCountablyGenerated` `Filter` `nhds` `instTopologicalSpace`	—	`exists_antitone_basis` `HasCountableBasis.isCountablyGenerated` `HasBasis.nhds` `HasAntitoneBasis.toHasBasis` `Set.to_countable` `SetCoe.countable` `instCountableNat`
`instT0Space` 📖	mathematical	—	`T0Space` `Filter` `instTopologicalSpace`	—	`LE.le.antisymm` `specializes_iff_le` `Inseparable.specializes` `Inseparable.symm`
`isInducing_nhds` 📖	mathematical	—	`Topology.IsInducing` `Filter` `instTopologicalSpace` `nhds`	—	`Topology.isInducing_iff_nhds` `nhds_def'` `nhds_nhds` `iInf_congr_Prop` `Iic_principal` `comap_iInf` `comap_principal` `IsOpen.interior_eq`
`isOpen_Iic_principal` 📖	mathematical	—	`IsOpen` `Filter` `instTopologicalSpace` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`Set.mem_range_self`
`isOpen_iff` 📖	mathematical	—	`IsOpen` `Filter` `instTopologicalSpace` `Set.iUnion` `Set` `Set.instMembership` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`TopologicalSpace.IsTopologicalBasis.open_iff_eq_sUnion` `isTopologicalBasis_Iic_principal` `Set.image_congr` `Set.sUnion_image`
`isOpen_setOf_mem` 📖	mathematical	—	`IsOpen` `Filter` `instTopologicalSpace` `setOf` `Set` `instMembership`	—	`Iic_principal` `isOpen_Iic_principal`
`isTopologicalBasis_Iic_principal` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `Filter` `instTopologicalSpace` `Set.range` `Set` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`Set.Iic_inter_Iic` `inf_principal` `Set.Subset.rfl` `Set.sUnion_eq_univ_iff` `principal_univ` `Set.mem_Iic` `le_top`
`mem_closure` 📖	mathematical	—	`Filter` `Set` `Set.instMembership` `closure` `instTopologicalSpace` `instMembership`	—	`closure_eq_compl_interior_compl`
`mem_interior` 📖	mathematical	—	`Filter` `Set` `Set.instMembership` `interior` `instTopologicalSpace` `instMembership` `Set.instHasSubset` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`mem_interior_iff_mem_nhds` `mem_nhds_iff`
`mem_nhds_iff` 📖	mathematical	—	`Set` `Filter` `instMembership` `nhds` `instTopologicalSpace` `Set.instHasSubset` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`HasBasis.mem_iff` `HasBasis.nhds` `basis_sets`
`mem_nhds_iff'` 📖	mathematical	—	`Set` `Filter` `instMembership` `nhds` `instTopologicalSpace` `Set.instMembership`	—	`HasBasis.mem_iff` `HasBasis.nhds'` `basis_sets`
`monotone_nhds` 📖	mathematical	—	`Monotone` `Filter` `PartialOrder.toPreorder` `instPartialOrder` `nhds` `instTopologicalSpace`	—	`Monotone.of_map_inf` `nhds_inf`
`nhds_atBot` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `atBot` `iInf` `instInfSet` `principal` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhds_atTop`
`nhds_atTop` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `atTop` `iInf` `instInfSet` `principal` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `Set.Ici`	—	`nhds_iInf` `nhds_principal`
`nhds_bot` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `Bot.bot` `instBot` `instPure`	—	`nhds_eq` `lift'_bot` `Monotone.Iic` `monotone_principal` `principal_empty` `Set.Iic_bot` `principal_singleton`
`nhds_eq` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `lift'` `Set` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder` `principal`	—	`TopologicalSpace.nhds_generateFrom` `iInf_congr_Prop` `iInf_and` `iInf_range`
`nhds_eq'` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `lift'` `setOf` `Set` `instMembership`	—	`Iic_principal` `nhds_eq`
`nhds_iInf` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `iInf` `instInfSet`	—	`nhds_eq` `lift'_iInf_of_map_univ` `Set.Iic_inter_Iic` `inf_principal` `principal_univ` `Set.Iic_top`
`nhds_inf` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `instInf`	—	`iInf_bool_eq` `nhds_iInf`
`nhds_mono` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `nhds` `instTopologicalSpace`	—	`Set.Iic_subset_Iic` `sInter_nhds` `Set.sInter_subset_sInter` `monotone_nhds`
`nhds_nhds` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `iInf` `Set` `instInfSet` `IsOpen` `Set.instMembership` `principal` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder`	—	`HasBasis.eq_biInf` `HasBasis.nhds` `nhds_basis_opens` `iInf_and` `iInf_comm`
`nhds_principal` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `principal` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder`	—	`HasBasis.eq_of_same_basis` `HasBasis.nhds` `hasBasis_principal`
`nhds_pure` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `instPure` `principal` `Set` `Set.instInsert` `Bot.bot` `instBot` `Set.instSingletonSet`	—	`principal_singleton` `nhds_principal` `Iic_pure`
`nhds_top` 📖	mathematical	—	`nhds` `Filter` `instTopologicalSpace` `Top.top` `instTop`	—	`nhds_eq` `lift'_top` `principal_univ` `Set.Iic_top`
`sInter_nhds` 📖	mathematical	—	`Set.sInter` `Filter` `setOf` `Set` `instMembership` `nhds` `instTopologicalSpace` `Set.Iic` `PartialOrder.toPreorder` `instPartialOrder`	—	`nhds_eq` `sInter_lift'_sets` `Monotone.Iic` `monotone_principal` `Set.iInter_congr_Prop`
`specializes_iff_le` 📖	mathematical	—	`Specializes` `Filter` `instTopologicalSpace` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	`closure_singleton`
`tendsto_nhds` 📖	mathematical	—	`Tendsto` `Filter` `nhds` `instTopologicalSpace` `Eventually` `Set` `instMembership`	—	`nhds_eq'`
`tendsto_nhds_atBot_iff` 📖	mathematical	—	`Tendsto` `Filter` `nhds` `instTopologicalSpace` `atBot` `Eventually` `Set` `instMembership` `Set.Iic`	—	`tendsto_nhds_atTop_iff`
`tendsto_nhds_atTop_iff` 📖	mathematical	—	`Tendsto` `Filter` `nhds` `instTopologicalSpace` `atTop` `Eventually` `Set` `instMembership` `Set.Ici`	—	`nhds_atTop`
`tendsto_pure_self` 📖	mathematical	—	`Tendsto` `Filter` `instPure` `nhds` `instTopologicalSpace`	—	`tendsto_nhds` `Eventually.mono`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds` 📖	mathematical	`Filter.HasBasis`	`Filter` `nhds` `Filter.instTopologicalSpace` `Set.Iic` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.principal`	—	`Filter.nhds_eq` `lift'` `Monotone.Iic` `Filter.monotone_principal`
`nhds'` 📖	mathematical	`Filter.HasBasis`	`Filter` `nhds` `Filter.instTopologicalSpace` `setOf` `Set` `Filter.instMembership`	—	`Filter.Iic_principal` `nhds`

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds` 📖	mathematical	`Filter.Tendsto` `nhds`	`Filter` `Filter.instTopologicalSpace`	—	`comp` `Continuous.tendsto` `Filter.continuous_nhds`

---

← Back to Index