Documentation Verification Report

List

📁 Source: Mathlib/Topology/List.lean

Statistics

Metric	Count
Definitions `instTopologicalSpace`, `instTopologicalSpaceList`	2
Theorems `cons`, `continuousAt_eraseIdx`, `continuous_eraseIdx`, `continuous_insertIdx`, `continuous_insertIdx'`, `tendsto_cons`, `tendsto_insertIdx`, `continuousAt_length`, `continuous_cons`, `continuous_eraseIdx`, `continuous_insertIdx`, `continuous_prod`, `continuous_sum`, `instDiscreteTopology`, `tendsto_cons`, `tendsto_cons_iff`, `tendsto_eraseIdx`, `tendsto_insertIdx`, `tendsto_insertIdx'`, `tendsto_nhds`, `tendsto_prod`, `tendsto_sum`, `nhds_cons`, `nhds_list`, `nhds_nil`	25
Total	27

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cons` 📖	—	`Filter.Tendsto` `nhds` `instTopologicalSpaceList`	—	—	`comp` `List.tendsto_cons` `prodMk`

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_length` 📖	mathematical	—	`ContinuousAt` `instTopologicalSpaceList` `instTopologicalSpaceNat`	—	`nhds_discrete` `instDiscreteTopologyNat` `tendsto_nhds` `Filter.tendsto_pure_pure` `Filter.Tendsto.comp` `Filter.tendsto_snd`
`continuous_cons` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `instTopologicalSpaceList`	—	`continuous_iff_continuousAt` `Filter.Tendsto.cons` `continuousAt_fst` `continuousAt_snd`
`continuous_eraseIdx` 📖	mathematical	—	`Continuous` `instTopologicalSpaceList`	—	`continuous_iff_continuousAt` `tendsto_eraseIdx`
`continuous_insertIdx` 📖	mathematical	—	`Continuous` `instTopologicalSpaceProd` `instTopologicalSpaceList`	—	`continuous_iff_continuousAt` `ContinuousAt.eq_1` `nhds_prod_eq` `tendsto_insertIdx'`
`continuous_prod` 📖	mathematical	—	`Continuous` `instTopologicalSpaceList` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`continuous_iff_continuousAt` `tendsto_prod`
`continuous_sum` 📖	mathematical	—	`Continuous` `instTopologicalSpaceList` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`continuous_iff_continuousAt` `tendsto_sum`
`instDiscreteTopology` 📖	mathematical	—	`DiscreteTopology` `instTopologicalSpaceList`	—	`discreteTopology_iff_nhds` `nhds_nil` `nhds_cons` `nhds_discrete` `Filter.instLawfulApplicative`
`tendsto_cons` 📖	mathematical	—	`Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `instTopologicalSpaceList`	—	`nhds_cons` `Filter.Tendsto.eq_1` `Filter.map_prod` `le_rfl`
`tendsto_cons_iff` 📖	mathematical	—	`Filter.Tendsto` `nhds` `instTopologicalSpaceList` `SProd.sprod` `Filter` `Filter.instSProd`	—	`nhds_cons` `Filter.prod_eq` `Filter.map_def` `Filter.seq_eq_filter_seq` `map_seq` `Filter.instLawfulApplicative` `Filter.instLawfulFunctor` `Filter.tendsto_map'_iff`
`tendsto_eraseIdx` 📖	mathematical	—	`Filter.Tendsto` `nhds` `instTopologicalSpaceList`	—	`nhds_nil` `tendsto_pure_nhds` `tendsto_cons_iff` `Filter.tendsto_snd` `Filter.Tendsto.cons` `Filter.tendsto_fst` `Filter.Tendsto.comp`
`tendsto_insertIdx` 📖	—	`Filter.Tendsto` `nhds` `instTopologicalSpaceList`	—	—	`Filter.Tendsto.comp` `tendsto_insertIdx'` `Filter.Tendsto.prodMk`
`tendsto_insertIdx'` 📖	mathematical	—	`Filter.Tendsto` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `instTopologicalSpaceList`	—	`tendsto_cons` `nhds_nil` `Filter.prod_pure` `nhds_cons` `Filter.prod_eq` `Filter.instLawfulApplicative` `Filter.instLawfulFunctor` `seq_map_assoc` `map_seq` `Filter.tendsto_map'_iff` `Filter.Tendsto.cons` `Filter.Tendsto.comp` `Filter.tendsto_fst` `Filter.tendsto_snd` `Filter.Tendsto.prodMk`
`tendsto_nhds` 📖	—	`Filter.Tendsto` `Filter` `Filter.instPure` `SProd.sprod` `Filter.instSProd` `nhds` `instTopologicalSpaceList`	—	—	`nhds_nil` `tendsto_cons_iff`
`tendsto_prod` 📖	mathematical	—	`Filter.Tendsto` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne` `nhds` `instTopologicalSpaceList`	—	`nhds_nil` `continuous_iff_continuousAt` `continuous_mul` `Filter.Tendsto.comp` `nhds_prod_eq` `ContinuousAt.eq_1` `Filter.Tendsto.prodMap` `Filter.tendsto_id`
`tendsto_sum` 📖	mathematical	—	`Filter.Tendsto` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero` `nhds` `instTopologicalSpaceList`	—	`nhds_nil` `Filter.tendsto_pure_left` `mem_of_mem_nhds` `tendsto_cons_iff` `continuous_iff_continuousAt` `continuous_add` `Filter.Tendsto.comp` `nhds_prod_eq` `ContinuousAt.eq_1` `Filter.Tendsto.prodMap` `Filter.tendsto_id`

List.Vector

Definitions

Name	Category	Theorems
`instTopologicalSpace` 📖	CompOp	5 math math: `continuous_insertIdx'`, `continuousAt_eraseIdx`, `tendsto_cons`, `continuous_eraseIdx`, `tendsto_insertIdx`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousAt_eraseIdx` 📖	mathematical	—	`ContinuousAt` `List.Vector` `instTopologicalSpace` `eraseIdx`	—	`ContinuousAt.eq_1` `eraseIdx.eq_1` `tendsto_subtype_rng` `eraseIdx_val` `Filter.Tendsto.comp` `List.tendsto_eraseIdx` `continuousAt_subtype_val`
`continuous_eraseIdx` 📖	mathematical	—	`Continuous` `List.Vector` `instTopologicalSpace` `eraseIdx`	—	`continuous_iff_continuousAt` `continuousAt_eraseIdx`
`continuous_insertIdx` 📖	mathematical	`Continuous` `List.Vector` `instTopologicalSpace`	`insertIdx`	—	`Continuous.comp` `continuous_insertIdx'` `Continuous.prodMk`
`continuous_insertIdx'` 📖	mathematical	—	`Continuous` `List.Vector` `instTopologicalSpaceProd` `instTopologicalSpace` `insertIdx`	—	`continuous_iff_continuousAt` `ContinuousAt.eq_1` `nhds_prod_eq` `tendsto_insertIdx`
`tendsto_cons` 📖	mathematical	—	`Filter.Tendsto` `List.Vector` `cons` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `instTopologicalSpace`	—	`tendsto_subtype_rng` `cons_val` `Filter.Tendsto.cons` `Filter.tendsto_fst` `Filter.Tendsto.comp` `continuousAt_subtype_val` `Filter.tendsto_snd`
`tendsto_insertIdx` 📖	mathematical	—	`Filter.Tendsto` `List.Vector` `insertIdx` `SProd.sprod` `Filter` `Filter.instSProd` `nhds` `instTopologicalSpace`	—	`insertIdx.eq_1` `tendsto_subtype_rng` `List.tendsto_insertIdx` `Filter.tendsto_fst` `Filter.Tendsto.comp` `continuousAt_subtype_val` `Filter.tendsto_snd`

(root)

Definitions

Name	Category	Theorems
`instTopologicalSpaceList` 📖	CompOp	16 math math: `nhds_cons`, `List.continuous_sum`, `List.tendsto_insertIdx'`, `nhds_nil`, `List.tendsto_cons_iff`, `List.continuous_insertIdx`, `List.tendsto_eraseIdx`, `List.tendsto_sum`, `List.tendsto_prod`, `List.instDiscreteTopology`, `nhds_list`, `List.continuous_cons`, `List.continuousAt_length`, `List.continuous_prod`, `List.continuous_eraseIdx`, `List.tendsto_cons`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`nhds_cons` 📖	mathematical	—	`nhds` `instTopologicalSpaceList` `Filter` `Filter.instAlternative` `Filter.instFunctor`	—	`nhds_list` `List.traverse_cons`
`nhds_list` 📖	mathematical	—	`nhds` `instTopologicalSpaceList` `Traversable.traverse` `instTraversableList` `Filter` `Filter.instAlternative`	—	`TopologicalSpace.nhds_mkOfNhds` `le_rfl` `Filter.seq_mono` `Filter.map_mono` `pure_le_nhds` `Filter.instLawfulApplicative` `Filter.mem_traverse_iff` `mem_nhds_iff` `Set.Subset.rfl` `Set.Subset.trans` `Set.seq_mono` `Set.image_mono` `Filter.mem_traverse` `List.Forall₂.imp` `IsOpen.mem_nhds` `Filter.mem_of_superset` `List.mem_traverse` `List.Forall₂.flip`
`nhds_nil` 📖	mathematical	—	`nhds` `instTopologicalSpaceList` `Filter` `Filter.instPure`	—	`nhds_list` `List.traverse_nil`

---

← Back to Index