LocallyFinite

📁 Source: Mathlib/Topology/LocallyFinite.lean

Statistics

Metric	Count
Definitions `LocallyFinite`, `LocallyFinite`	2
Theorems `locallyFinite_comp_iff`, `closure`, `closure_iUnion`, `comp_injOn`, `comp_injective`, `continuous`, `continuous'`, `continuousOn_iUnion`, `continuousOn_iUnion'`, `eventually_smallSets`, `eventually_subset`, `exists_forall_eventually_atTop_eventuallyEq`, `exists_forall_eventually_atTop_eventually_eq'`, `exists_forall_eventually_eq_prod`, `exists_mem_basis`, `iInter_compl_mem_nhds`, `isClosed_iUnion`, `nhdsWithin_iUnion`, `of_comp_surjective`, `on_range`, `option_elim'`, `point_finite`, `preimage_continuous`, `prod_left`, `prod_right`, `subset`, `sumElim`, `locallyFinite_iff_smallSets`, `locallyFinite_of_finite`, `locallyFinite_option`, `locallyFinite_sum`	31
Total	33

Equiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyFinite_comp_iff` 📖	mathematical	—	`LocallyFinite` `Set` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `instEquivLike`	—	`apply_symm_apply` `LocallyFinite.comp_injective` `injective`

LocallyFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure` 📖	mathematical	`LocallyFinite`	`closure`	—	`interior_mem_nhds` `Set.Finite.subset` `Set.Nonempty.mono` `Set.inter_subset_inter_right` `interior_subset` `Set.Nonempty.of_closure` `IsOpen.closure_inter` `isOpen_interior`
`closure_iUnion` 📖	mathematical	`LocallyFinite`	`closure` `Set.iUnion`	—	`Set.ext` `nhdsWithin_iUnion`
`comp_injOn` 📖	mathematical	`LocallyFinite` `Set.InjOn` `setOf` `Set.Nonempty`	`Set`	—	`Set.Finite.preimage` `Set.InjOn.mono` `Set.Nonempty.left`
`comp_injective` 📖	mathematical	`LocallyFinite`	`Set`	—	`comp_injOn` `Function.Injective.injOn`
`continuous` 📖	mathematical	`LocallyFinite` `Set.iUnion` `Set.univ` `IsClosed` `ContinuousOn`	`Continuous`	—	`continuousOn_univ` `continuousOn_iUnion`
`continuous'` 📖	mathematical	`LocallyFinite` `Set.iUnion` `Set.univ` `ContinuousWithinAt`	`Continuous`	—	`continuousOn_univ` `continuousOn_iUnion'`
`continuousOn_iUnion` 📖	mathematical	`LocallyFinite` `IsClosed` `ContinuousOn`	`Set.iUnion`	—	`continuousOn_iUnion'` `IsClosed.closure_subset`
`continuousOn_iUnion'` 📖	mathematical	`LocallyFinite` `ContinuousWithinAt`	`ContinuousOn` `Set.iUnion`	—	`ContinuousWithinAt.eq_1` `nhdsWithin_iUnion` `Filter.tendsto_iSup` `Filter.not_neBot` `mem_closure_iff_nhdsWithin_neBot` `Filter.tendsto_bot`
`eventually_smallSets` 📖	mathematical	`LocallyFinite`	`Filter.Eventually` `Set` `Set.Finite` `setOf` `Set.Nonempty` `Set.instInter` `Filter.smallSets` `nhds`	—	`locallyFinite_iff_smallSets`
`eventually_subset` 📖	mathematical	`LocallyFinite` `IsClosed`	`Filter.Eventually` `Set` `Set.instHasSubset` `setOf` `Set.instMembership` `nhds`	—	`Filter.mp_mem` `iInter_compl_mem_nhds` `Filter.univ_mem'` `not_imp_not`
`exists_forall_eventually_atTop_eventuallyEq` 📖	mathematical	`LocallyFinite` `setOf`	`Filter.Eventually` `Filter.EventuallyEq` `nhds` `Filter.atTop` `Nat.instPreorder`	—	`exists_forall_eventually_atTop_eventually_eq'`
`exists_forall_eventually_atTop_eventually_eq'` 📖	mathematical	`LocallyFinite` `setOf`	`Filter.Eventually` `nhds` `Filter.atTop` `Nat.instPreorder`	—	`Filter.Eventually.curry` `exists_forall_eventually_eq_prod`
`exists_forall_eventually_eq_prod` 📖	mathematical	`LocallyFinite` `setOf`	`Filter.Eventually` `SProd.sprod` `Filter` `Filter.instSProd` `Filter.atTop` `Nat.instPreorder` `nhds`	—	`by_contra` `LT.lt.not_ge` `GT.gt.lt` `Nat.le_induction` `Filter.mp_mem` `Filter.prod_mem_prod` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `Nat.instNoMaxOrder` `Filter.univ_mem'` `le_max_left` `le_max_right` `mem_of_mem_nhds` `Set.Finite.bddAbove` `SemilatticeSup.instIsDirectedOrder`
`exists_mem_basis` 📖	mathematical	`LocallyFinite` `Filter.HasBasis` `nhds`	`Set.Finite` `setOf` `Set.Nonempty` `Set` `Set.instInter`	—	`Filter.HasBasis.eventually_iff` `Filter.HasBasis.smallSets` `eventually_smallSets` `Set.Subset.rfl`
`iInter_compl_mem_nhds` 📖	mathematical	`LocallyFinite` `IsClosed`	`Set` `Filter` `Filter.instMembership` `nhds` `Set.iInter` `Set.instMembership` `Compl.compl` `Set.instCompl`	—	`IsOpen.mem_nhds` `isClosed_iUnion` `comp_injective` `Subtype.val_injective` `Set.iInter_subtype` `Set.compl_iUnion` `isOpen_compl_iff` `Set.mem_iInter₂`
`isClosed_iUnion` 📖	mathematical	`LocallyFinite` `IsClosed`	`Set.iUnion`	—	`closure_iUnion` `IsClosed.closure_eq`
`nhdsWithin_iUnion` 📖	mathematical	`LocallyFinite`	`nhdsWithin` `Set.iUnion` `iSup` `Filter` `Filter.instSupSet`	—	`le_antisymm` `Set.iUnion_inter` `nhdsWithin_inter_of_mem'` `nhdsWithin_le_nhds` `Set.iUnion_nonempty_self` `nhdsWithin_biUnion` `iSup₂_le_iSup` `iSup_mono` `nhdsWithin_mono` `Set.inter_subset_left` `Monotone.le_map_iSup`
`of_comp_surjective` 📖	—	`LocallyFinite` `Set`	—	—	`Function.surjInv_eq` `comp_injective` `Function.injective_surjInv`
`on_range` 📖	mathematical	`LocallyFinite`	`Set` `Set.instMembership` `Set.range`	—	`of_comp_surjective` `Set.rangeFactorization_surjective`
`option_elim'` 📖	mathematical	`LocallyFinite`	`Option.elim'` `Set`	—	`locallyFinite_option`
`point_finite` 📖	mathematical	`LocallyFinite`	`Set.Finite` `setOf` `Set` `Set.instMembership`	—	`Set.Finite.subset` `mem_of_mem_nhds`
`preimage_continuous` 📖	mathematical	`LocallyFinite` `Continuous`	`Set.preimage`	—	`Continuous.continuousAt` `Set.Finite.subset`
`prod_left` 📖	mathematical	`LocallyFinite`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`subset` `preimage_continuous` `continuous_snd` `Set.prod_subset_preimage_snd`
`prod_right` 📖	mathematical	`LocallyFinite`	`instTopologicalSpaceProd` `SProd.sprod` `Set` `Set.instSProd`	—	`subset` `preimage_continuous` `continuous_fst` `Set.prod_subset_preimage_fst`
`subset` 📖	—	`LocallyFinite` `Set` `Set.instHasSubset`	—	—	`Set.Finite.subset` `Set.Nonempty.mono` `Set.inter_subset_inter` `Set.Subset.rfl`
`sumElim` 📖	mathematical	`LocallyFinite`	`Set`	—	`locallyFinite_sum`

SimpleGraph

Definitions

Name	Category	Theorems
`LocallyFinite` 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
`LocallyFinite` 📖	MathDef	26 math math: `locallyFinite_iff_smallSets`, `SmoothPartitionOfUnity.locallyFinite`, `SmoothPartitionOfUnity.locallyFinite'`, `precise_refinement`, `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`, `PartitionOfUnity.locallyFinite`, `locallyFinite_sum`, `SmoothBumpCovering.locallyFinite'`, `locallyFinite_of_finite`, `exists_locallyFinite_iUnion_eq_ball_radius_lt`, `ParacompactSpace.locallyFinite_refinement`, `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis_set`, `BumpCovering.locallyFinite`, `PartitionOfUnity.locallyFinite'`, `LocallyFinite.Realizer.to_locallyFinite`, `PartitionOfUnity.locallyFinite_tsupport`, `BumpCovering.locallyFinite_tsupport`, `locallyFinite_support_iff`, `Equiv.locallyFinite_comp_iff`, `locallyFinite_option`, `locallyFinite_iff_exists_realizer`, `SmoothBumpCovering.locallyFinite`, `precise_refinement_set`, `exists_locallyFinite_subset_iUnion_ball_radius_lt`, `BumpCovering.locallyFinite'`, `locallyFinite_mulSupport_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`locallyFinite_iff_smallSets` 📖	mathematical	—	`LocallyFinite` `Filter.Eventually` `Set` `Set.Finite` `setOf` `Set.Nonempty` `Set.instInter` `Filter.smallSets` `nhds`	—	`Filter.eventually_smallSets'` `Set.Finite.subset` `Set.Nonempty.mono` `Set.inter_subset_inter_right`
`locallyFinite_of_finite` 📖	mathematical	—	`LocallyFinite`	—	`Filter.univ_mem` `Set.toFinite` `Subtype.finite`
`locallyFinite_option` 📖	mathematical	—	`LocallyFinite` `Set`	—	`Equiv.locallyFinite_comp_iff` `locallyFinite_sum` `Finite.of_fintype`
`locallyFinite_sum` 📖	mathematical	—	`LocallyFinite` `Set`	—	—

---

← Back to Index