Documentation Verification Report

DerivedSet

📁 Source: Mathlib/Topology/DerivedSet.lean

Statistics

Metric	Count
Definitions `derivedSet`	1
Theorems `map`, `image_derivedSet`, `inter_derivedSet_nonempty`, `closure_eq_self_union_derivedSet`, `derivedSet_closure`, `derivedSet_mono`, `derivedSet_subset_closure`, `derivedSet_union`, `isClosed_derivedSet`, `isClosed_iff_derivedSet_subset`, `mem_derivedSet`, `perfect_iff_eq_derivedSet`, `preperfect_iff_subset_derivedSet`	13
Total	14

AccPt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map` 📖	mathematical	`ContinuousAt`	`AccPt` `Filter.map`	—	`Filter.NeBot.mono` `Filter.map_neBot` `Filter.map_inf` `inf_le_inf` `tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within` `ContinuousAt.continuousWithinAt` `eventually_mem_nhdsWithin` `le_refl`

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`image_derivedSet` 📖	mathematical	`Continuous`	`Set` `Set.instHasSubset` `Set.image` `derivedSet`	—	`Filter.map_principal` `AccPt.map` `continuousAt`

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inter_derivedSet_nonempty` 📖	—	`IsPreconnected` `Set` `Set.instHasSubset` `Set.instUnion` `Set.Nonempty` `Set.instInter` `derivedSet`	—	—	`isPreconnected_closed_iff` `preperfect_of_nontrivial` `derivedSet_union` `derivedSet_mono` `Set.Nonempty.exists_eq_singleton_or_nontrivial` `Set.Nonempty.left` `Set.singleton_inter_of_mem`

(root)

Definitions

Name	Category	Theorems
`derivedSet` 📖	CompOp	11 math math: `derivedSet_union`, `isClosed_iff_derivedSet_subset`, `mem_derivedSet`, `closure_eq_self_union_derivedSet`, `Continuous.image_derivedSet`, `derivedSet_mono`, `derivedSet_closure`, `perfect_iff_eq_derivedSet`, `preperfect_iff_subset_derivedSet`, `derivedSet_subset_closure`, `isClosed_derivedSet`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`closure_eq_self_union_derivedSet` 📖	mathematical	—	`closure` `Set` `Set.instUnion` `derivedSet`	—	`Set.ext` `closure_eq_cluster_pts`
`derivedSet_closure` 📖	mathematical	—	`derivedSet` `closure`	—	`le_antisymm` `mem_derivedSet` `AccPt.eq_1` `Filter.HasBasis.inf_principal_neBot_iff` `nhdsWithin_basis_open` `mem_closure_iff` `Set.Nonempty.some_mem` `IsOpen.inter` `isOpen_compl_singleton` `derivedSet_mono` `subset_closure`
`derivedSet_mono` 📖	mathematical	`Set` `Set.instHasSubset`	`derivedSet`	—	`AccPt.mono` `Filter.le_principal_iff` `Filter.mem_principal`
`derivedSet_subset_closure` 📖	mathematical	—	`Set` `Set.instHasSubset` `derivedSet` `closure`	—	`mem_closure_iff_clusterPt` `AccPt.clusterPt`
`derivedSet_union` 📖	mathematical	—	`derivedSet` `Set` `Set.instUnion`	—	`Set.ext`
`isClosed_derivedSet` 📖	mathematical	—	`IsClosed` `derivedSet`	—	`derivedSet_closure` `isClosed_iff_derivedSet_subset` `derivedSet_mono`
`isClosed_iff_derivedSet_subset` 📖	mathematical	—	`IsClosed` `Set` `Set.instHasSubset` `derivedSet`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `derivedSet_subset_closure` `IsClosed.closure_subset` `isClosed_iff_clusterPt` `Set.diff_singleton_eq_self` `accPt_principal_iff_clusterPt`
`mem_derivedSet` 📖	mathematical	—	`Set` `Set.instMembership` `derivedSet` `AccPt` `Filter.principal`	—	—
`perfect_iff_eq_derivedSet` 📖	mathematical	—	`Perfect` `derivedSet`	—	`perfect_def` `isClosed_iff_derivedSet_subset` `preperfect_iff_subset_derivedSet` `subset_antisymm_iff` `Set.instReflSubset` `Set.instAntisymmSubset`
`preperfect_iff_subset_derivedSet` 📖	mathematical	—	`Preperfect` `Set` `Set.instHasSubset` `derivedSet`	—	—

---

← Back to Index