Documentation Verification Report

Subsingleton

📁 Source: Mathlib/Order/Filter/Subsingleton.lean

Statistics

Metric	Count
Definitions `Subsingleton`	1
Theorems `subsingleton_iff`, `anti`, `exists_eq_pure`, `exists_le_pure`, `isCountablyGenerated`, `map`, `of_subsingleton`, `prod`, `subsingleton_bot`, `subsingleton_iff_bot_or_pure`, `subsingleton_iff_exists_le_pure`, `subsingleton_iff_exists_singleton_mem`, `subsingleton_pure`	13
Total	14

Filter

Definitions

Name	Category	Theorems
`Subsingleton` 📖	MathDef	8 math math: `Subsingleton.of_subsingleton`, `subsingleton_iff_exists_le_pure`, `subsingleton_iff_bot_or_pure`, `HasBasis.subsingleton_iff`, `eventuallyConst_id`, `subsingleton_bot`, `subsingleton_iff_exists_singleton_mem`, `subsingleton_pure`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_bot` 📖	mathematical	—	`Subsingleton` `Bot.bot` `Filter` `instBot`	—	`Set.subsingleton_empty`
`subsingleton_iff_bot_or_pure` 📖	mathematical	—	`Subsingleton` `Bot.bot` `Filter` `instBot` `instPure`	—	`Subsingleton.exists_eq_pure` `eq_or_neBot`
`subsingleton_iff_exists_le_pure` 📖	mathematical	—	`Subsingleton` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instPure`	—	`eq_or_neBot` `NeBot.ne` `NeBot.le_pure_iff`
`subsingleton_iff_exists_singleton_mem` 📖	mathematical	—	`Subsingleton` `Set` `Filter` `instMembership` `Set.instSingletonSet`	—	—
`subsingleton_pure` 📖	mathematical	—	`Subsingleton` `Filter` `instPure`	—	`Set.subsingleton_singleton`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subsingleton_iff` 📖	mathematical	`Filter.HasBasis`	`Filter.Subsingleton` `Set.Subsingleton`	—	`exists_iff` `Set.Subsingleton.anti`

Filter.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	—	`Filter.Subsingleton` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	—
`exists_eq_pure` 📖	mathematical	`Filter.Subsingleton`	`Filter` `Filter.instPure`	—	`Set.exists_eq_singleton_iff_nonempty_subsingleton` `Filter.nonempty_of_mem` `Filter.NeBot.le_pure_iff` `Filter.le_pure_iff`
`exists_le_pure` 📖	mathematical	`Filter.Subsingleton`	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.instPure`	—	`Filter.subsingleton_iff_exists_le_pure`
`isCountablyGenerated` 📖	mathematical	`Filter.Subsingleton`	`Filter.IsCountablyGenerated`	—	`Filter.subsingleton_iff_bot_or_pure` `Filter.isCountablyGenerated_bot` `Filter.isCountablyGenerated_pure`
`map` 📖	mathematical	`Filter.Subsingleton`	`Filter.map`	—	`Filter.image_mem_map` `Set.Subsingleton.image`
`of_subsingleton` 📖	mathematical	—	`Filter.Subsingleton`	—	`Filter.univ_mem` `Set.subsingleton_univ`
`prod` 📖	mathematical	`Filter.Subsingleton`	`SProd.sprod` `Filter` `Filter.instSProd`	—	`Filter.prod_mem_prod` `Set.Subsingleton.prod`

---

← Back to Index