Documentation Verification Report

ShrinkingLemma

📁 Source: Mathlib/Topology/ShrinkingLemma.lean

Statistics

Metric	Count
Definitions `PartialRefinement`, `carrier`, `chainSup`, `chainSupCarrier`, `find`, `instCoeFunForallSet`, `instPartialOrder`, `toFun`	8
Theorems `apply_eq`, `apply_eq_of_chain`, `closure_subset`, `exists_gt`, `ext`, `ext_iff`, `find_apply_of_mem`, `find_mem`, `isOpen`, `le_chainSup`, `mem_find_carrier_iff`, `pred_of_mem`, `subset`, `subset_iUnion`, `exists_gt_t2space`, `exists_iUnion_eq_closed_subset`, `exists_iUnion_eq_closure_subset`, `exists_subset_iUnion_closed_subset`, `exists_subset_iUnion_closure_subset`, `exists_subset_iUnion_closure_subset_t2space`, `exists_subset_iUnion_compact_subset_t2space`	21
Total	29

ShrinkingLemma

Definitions

Name	Category	Theorems
`PartialRefinement` 📖	CompData	2 math math: `PartialRefinement.exists_gt`, `exists_gt_t2space`

ShrinkingLemma.PartialRefinement

Definitions

Name	Category	Theorems
`carrier` 📖	CompOp	2 math math: `ext_iff`, `mem_find_carrier_iff`
`chainSup` 📖	CompOp	1 math math: `le_chainSup`
`chainSupCarrier` 📖	CompOp	1 math math: `mem_find_carrier_iff`
`find` 📖	CompOp	3 math math: `find_apply_of_mem`, `find_mem`, `mem_find_carrier_iff`
`instCoeFunForallSet` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	2 math math: `exists_gt`, `exists_gt_t2space`
`toFun` 📖	CompOp	10 math math: `subset`, `apply_eq`, `find_apply_of_mem`, `pred_of_mem`, `closure_subset`, `exists_gt_t2space`, `subset_iUnion`, `ext_iff`, `isOpen`, `apply_eq_of_chain`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_eq` 📖	mathematical	`Set` `Set.instMembership` `carrier`	`toFun`	—	—
`apply_eq_of_chain` 📖	mathematical	`IsChain` `ShrinkingLemma.PartialRefinement` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set` `Set.instMembership` `carrier`	`toFun`	—	`IsChain.total` `instReflLe`
`closure_subset` 📖	mathematical	`Set` `Set.instMembership` `carrier`	`Set.instHasSubset` `closure` `toFun`	—	—
`exists_gt` 📖	mathematical	`Set` `Set.instMembership` `carrier` `Top.top` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	`ShrinkingLemma.PartialRefinement` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrder`	—	`Set.mem_iUnion` `subset_iUnion` `em` `IsClosed.inter` `isClosed_biInter` `isClosed_compl_iff` `isOpen` `normal_exists_closure_subset` `eq_or_ne` `Function.update_self` `Function.update_of_ne` `Set.mem_biInter` `Mathlib.Tactic.Push.not_and_eq` `apply_eq` `closure_subset` `Set.mem_insert_iff` `Set.subset_insert` `Set.mem_insert`
`ext` 📖	—	`toFun` `carrier`	—	—	—
`ext_iff` 📖	mathematical	—	`toFun` `carrier`	—	`ext`
`find_apply_of_mem` 📖	mathematical	`IsChain` `ShrinkingLemma.PartialRefinement` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set.Nonempty` `Set` `Set.instMembership` `carrier`	`toFun` `find`	—	`apply_eq_of_chain` `find_mem` `mem_find_carrier_iff` `Set.mem_iUnion₂`
`find_mem` 📖	mathematical	`Set.Nonempty` `ShrinkingLemma.PartialRefinement`	`Set` `Set.instMembership` `find`	—	`find.eq_1` `Set.Nonempty.some_mem`
`isOpen` 📖	mathematical	—	`IsOpen` `toFun`	—	—
`le_chainSup` 📖	mathematical	`IsChain` `ShrinkingLemma.PartialRefinement` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Set.Nonempty` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.instHasSubset` `Set.iUnion`	`chainSup`	—	`Set.mem_biUnion` `find_apply_of_mem`
`mem_find_carrier_iff` 📖	mathematical	`Set.Nonempty` `ShrinkingLemma.PartialRefinement`	`Set` `Set.instMembership` `carrier` `find` `chainSupCarrier`	—	`find.eq_1` `Set.mem_iUnion₂` `Mathlib.Tactic.Push.not_and_eq` `Set.Nonempty.some_mem`
`pred_of_mem` 📖	mathematical	`Set` `Set.instMembership` `carrier`	`toFun`	—	—
`subset` 📖	mathematical	—	`Set` `Set.instHasSubset` `toFun`	—	`HasSubset.Subset.trans` `Set.instIsTransSubset` `subset_closure` `closure_subset` `Eq.le` `apply_eq`
`subset_iUnion` 📖	mathematical	—	`Set` `Set.instHasSubset` `Set.iUnion` `toFun`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_gt_t2space` 📖	mathematical	`IsCompact` `Set` `Set.instMembership` `ShrinkingLemma.PartialRefinement.carrier` `closure`	`ShrinkingLemma.PartialRefinement` `Preorder.toLT` `PartialOrder.toPreorder` `ShrinkingLemma.PartialRefinement.instPartialOrder` `ShrinkingLemma.PartialRefinement.toFun`	—	`IsCompact.of_isClosed_subset` `isOpen_biUnion` `ShrinkingLemma.PartialRefinement.isOpen` `IsClosed.inter` `IsCompact.isClosed` `IsOpen.isClosed_compl` `Set.inter_subset_left` `Set.notMem_of_mem_compl` `Set.mem_of_mem_inter_right` `Set.compl_iUnion` `Set.mem_iInter₂` `Set.mem_iUnion` `ShrinkingLemma.PartialRefinement.subset_iUnion` `Set.mem_of_mem_inter_left` `exists_open_between_and_isCompact_closure` `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `T2Space.r1Space` `eq_or_ne` `Function.update_self` `Function.update_of_ne` `Set.mem_iInter₂_of_mem` `Mathlib.Tactic.Push.not_and_eq` `subset_trans` `Set.instIsTransSubset` `ShrinkingLemma.PartialRefinement.subset` `ShrinkingLemma.PartialRefinement.closure_subset` `Set.mem_insert_iff` `ShrinkingLemma.PartialRefinement.pred_of_mem` `ShrinkingLemma.PartialRefinement.apply_eq` `Set.subset_insert` `Set.mem_insert`
`exists_iUnion_eq_closed_subset` 📖	mathematical	`IsOpen` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.iUnion` `Set.univ`	`IsClosed` `Set.instHasSubset`	—	`exists_subset_iUnion_closed_subset` `isClosed_univ` `Eq.ge` `Set.univ_subset_iff`
`exists_iUnion_eq_closure_subset` 📖	mathematical	`IsOpen` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.iUnion` `Set.univ`	`Set.instHasSubset` `closure`	—	`exists_subset_iUnion_closure_subset` `isClosed_univ` `Eq.ge` `Set.univ_subset_iff`
`exists_subset_iUnion_closed_subset` 📖	mathematical	`IsOpen` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.instHasSubset` `Set.iUnion`	`IsClosed`	—	`exists_subset_iUnion_closure_subset` `Set.Subset.trans` `Set.iUnion_mono` `subset_closure` `isClosed_closure`
`exists_subset_iUnion_closure_subset` 📖	mathematical	`IsOpen` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.instHasSubset` `Set.iUnion`	`closure`	—	`ShrinkingLemma.PartialRefinement.le_chainSup` `zorn_le_nonempty` `ShrinkingLemma.PartialRefinement.exists_gt` `IsMax.not_lt` `ShrinkingLemma.PartialRefinement.subset_iUnion` `ShrinkingLemma.PartialRefinement.isOpen` `ShrinkingLemma.PartialRefinement.closure_subset`
`exists_subset_iUnion_closure_subset_t2space` 📖	mathematical	`IsCompact` `IsOpen` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.instHasSubset` `Set.iUnion`	`closure`	—	`ShrinkingLemma.PartialRefinement.le_chainSup` `zorn_le_nonempty` `exists_gt_t2space` `IsMax.not_lt` `ShrinkingLemma.PartialRefinement.subset_iUnion` `ShrinkingLemma.PartialRefinement.isOpen` `ShrinkingLemma.PartialRefinement.closure_subset` `ShrinkingLemma.PartialRefinement.pred_of_mem`
`exists_subset_iUnion_compact_subset_t2space` 📖	mathematical	`IsCompact` `IsOpen` `Set.Finite` `setOf` `Set` `Set.instMembership` `Set.instHasSubset` `Set.iUnion`	`IsClosed`	—	`exists_subset_iUnion_closure_subset_t2space` `Set.Subset.trans` `Set.iUnion_mono` `subset_closure`

---

← Back to Index