Subsingleton

📁 Source: Mathlib/Data/Set/Subsingleton.lean

Statistics

Metric	Count
Definitions `Subsingleton`	1
Theorems `exists_eq_singleton_or_nontrivial`, `choose_fst_mem`, `choose_fst_ne_choose_snd`, `choose_snd_mem`, `coe_sort`, `exists_lt`, `exists_ne`, `mono`, `ne_empty`, `ne_singleton`, `nonempty`, `not_subset_empty`, `not_subset_singleton`, `not_subsingleton`, `pair_subset`, `anti`, `antitoneOn`, `coe_sort`, `denselyOrdered`, `eq_empty_or_singleton`, `eq_singleton_of_mem`, `induction_on`, `inter_singleton`, `monotoneOn`, `not_nontrivial`, `singleton_inter`, `strictAntiOn`, `strictMonoOn`, `antitoneOn_singleton`, `eq_empty_or_singleton_of_subsingleton`, `eq_empty_or_singleton_of_unique`, `eq_singleton_or_nontrivial`, `exists_eq_singleton_iff_nonempty_subsingleton`, `monotoneOn_singleton`, `nontrivial_coe_sort`, `nontrivial_iff_exists_lt`, `nontrivial_iff_exists_ne`, `nontrivial_iff_ne_singleton`, `nontrivial_iff_pair_subset`, `nontrivial_mono`, `nontrivial_of_exists_lt`, `nontrivial_of_exists_ne`, `nontrivial_of_lt`, `nontrivial_of_mem_mem_ne`, `nontrivial_of_nontrivial`, `nontrivial_of_nontrivial_coe`, `nontrivial_of_pair_subset`, `nontrivial_of_univ_nontrivial`, `nontrivial_pair`, `nontrivial_univ`, `nontrivial_univ_iff`, `not_nontrivial_empty`, `not_nontrivial_iff`, `not_nontrivial_singleton`, `not_subsingleton_iff`, `singleton_ne_univ`, `singleton_ssubset_univ`, `strictAntiOn_singleton`, `strictMonoOn_singleton`, `subsingleton_coe`, `subsingleton_coe_of_subsingleton`, `subsingleton_empty`, `subsingleton_iff_singleton`, `subsingleton_isBot`, `subsingleton_isTop`, `subsingleton_of_forall_eq`, `subsingleton_of_subset_singleton`, `subsingleton_of_subsingleton`, `subsingleton_of_subsingleton_inter_left`, `subsingleton_of_subsingleton_inter_right`, `subsingleton_of_univ_subsingleton`, `subsingleton_or_nontrivial`, `subsingleton_singleton`, `subsingleton_univ`, `subsingleton_univ_iff`, `univ_eq_true_false`, `univ_set_eq_singleton_empty_iff`, `univ_set_of_isEmpty`	78
Total	79

Set

Definitions

Name	Category	Theorems
`Subsingleton` 📖	MathDef	100 math math: `Pi.subsingleton_support_single`, `not_subsingleton_iff`, `inter_subsingleton_of_isAntichain_of_isChain`, `subsingleton_univ`, `MulAction.IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_alternatingGroup_le`, `subsingleton_toFinset_iff`, `vectorSpan_eq_bot_iff_subsingleton`, `infsep_zero_iff_subsingleton_of_finite`, `SimpleGraph.IsClique.subsingleton`, `Cardinal.mk_le_one_iff_set_subsingleton`, `Irreducible.subsingleton_isRoot`, `subsingleton_univ_iff`, `Subsingleton.singleton_inter`, `subsingleton_of_einfsep_eq_top`, `AddAction.IsBlock.subsingleton_or_eq_univ`, `subsingleton_isTop`, `subsingleton_range`, `MulAction.IsBlock.subsingleton_of_card_lt`, `IsDiscrete.subsingleton_of_isPreirreducible`, `Pi.subsingleton_mulSupport_mulSingle`, `isChain_and_isAntichain_iff_subsingleton`, `ncard_le_one_iff_subsingleton`, `SimpleGraph.Subgraph.Preconnected.degree_zero_iff`, `MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le`, `AffineIndependent.vectorSpan_image_eq_iff`, `subsingleton_or_nontrivial`, `subsingleton_image_closure_of_finite_of_isPreirreducible`, `Filter.exists_subsingleton_mem_of_forall_separating`, `einfsep_eq_top_iff`, `IsStrongAntichain.subsingleton`, `IsPreconnected.subsingleton`, `Sized.subsingleton'`, `subsingleton_zero_smul_set`, `Part.subsingleton`, `Metric.subsingleton_sphere`, `Function.Injective.subsingleton_image_iff`, `subsingleton_singleton`, `Filter.HasBasis.subsingleton_iff`, `AddAction.IsBlock.subsingleton_of_card_lt`, `SimpleGraph.edgeDisjointTriangles_iff_mem_sym2_subsingleton`, `subsingleton_of_forall_eq`, `minimal_nonempty_open_subsingleton`, `Polynomial.subsingleton_isRoot_of_natDegree_eq_one`, `pairwise_bot_iff`, `WithZero.denselyOrdered_set_iff_subsingleton`, `subsingleton_Icc_iff`, `subsingleton_of_subsingleton`, `Finite.infsep_zero_iff_subsingleton`, `UniqueAdd.set_subsingleton`, `Equiv.Perm.IsCycleOn.subsingleton`, `IsPreirreducible.subsingleton`, `subsingleton_closure`, `exists_eq_singleton_iff_nonempty_subsingleton`, `Nontrivial.not_subsingleton`, `SimpleGraph.EdgeDisjointTriangles.mem_sym2_subsingleton`, `IsAntichain.subsingleton`, `subsingleton_empty`, `Sized.subsingleton`, `SimpleGraph.isClique_bot_iff`, `not_nontrivial_iff`, `inter_subsingleton_of_isChain_of_isAntichain`, `subsingleton_iff_singleton`, `subsingleton_botSet`, `Finset.infsep_zero_iff_subsingleton`, `subsingleton_of_isChain_of_isAntichain`, `offDiag_eq_empty`, `subsingleton_of_isLUB_le_isGLB`, `subsingleton_of_subset_singleton`, `subsingleton_coe`, `UniqueMul.set_subsingleton`, `MulAction.IsBlock.subsingleton_or_eq_univ`, `RelSeries.subsingleton_of_length_eq_zero`, `Metric.ediam_eq_zero_iff`, `WithTop.denselyOrdered_set_iff_subsingleton`, `minimal_nonempty_closed_subsingleton`, `Equiv.Perm.isCycleOn_one`, `RelSeries.length_eq_zero`, `Finpartition.parts_top_subsingleton`, `denselyOrdered_set_iff_subsingleton`, `subsingleton_setOf_mem_iff_pairwise_disjoint`, `Subsingleton.inter_singleton`, `Pairwise.subsingleton`, `totallyDisconnectedSpace_iff_connectedComponent_subsingleton`, `IsBlock.subsingleton_of_ssubset_compl_of_stabilizer_le`, `addDissociated_iff_sum_eq_subsingleton`, `WithBot.denselyOrdered_set_iff_subsingleton`, `EMetric.diam_eq_zero_iff`, `subsingleton_isBot`, `SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint`, `MulAction.subsingleton_orbit_iff_mem_fixedPoints`, `AddAction.subsingleton_orbit_iff_mem_fixedPoints`, `SimpleGraph.isClique_map_iff`, `Filter.exists_subset_subsingleton_mem_of_forall_separating`, `encard_le_one_iff_subsingleton`, `Metric.subsingleton_closedBall`, `subsingleton_Icc_of_ge`, `Finset.powersetCard_empty_subsingleton`, `isPreirreducible_iff_subsingleton`, `mulDissociated_iff_sum_eq_subsingleton`, `MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_Perm_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`antitoneOn_singleton` 📖	mathematical	—	`AntitoneOn` `Set` `instSingletonSet`	—	`Subsingleton.antitoneOn` `subsingleton_singleton`
`eq_empty_or_singleton_of_subsingleton` 📖	mathematical	—	`Set` `instEmptyCollection` `instSingletonSet`	—	`Subsingleton.eq_empty_or_singleton` `subsingleton_of_subsingleton`
`eq_empty_or_singleton_of_unique` 📖	mathematical	—	`Set` `instEmptyCollection` `instSingletonSet` `Unique.instInhabited`	—	`Unique.eq_default` `eq_empty_or_singleton_of_subsingleton` `Unique.instSubsingleton`
`eq_singleton_or_nontrivial` 📖	mathematical	`Set` `instMembership`	`instSingletonSet` `Nontrivial`	—	`subsingleton_iff_singleton` `subsingleton_or_nontrivial`
`exists_eq_singleton_iff_nonempty_subsingleton` 📖	mathematical	—	`Set` `instSingletonSet` `Nonempty` `Subsingleton`	—	`singleton_nonempty` `subsingleton_singleton` `Subsingleton.eq_empty_or_singleton` `Nonempty.ne_empty`
`monotoneOn_singleton` 📖	mathematical	—	`MonotoneOn` `Set` `instSingletonSet`	—	`Subsingleton.monotoneOn` `subsingleton_singleton`
`nontrivial_coe_sort` 📖	mathematical	—	`Nontrivial` `Elem` `Nontrivial`	—	—
`nontrivial_iff_exists_lt` 📖	mathematical	—	`Nontrivial` `Set` `instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`Nontrivial.exists_lt` `nontrivial_of_exists_lt`
`nontrivial_iff_exists_ne` 📖	mathematical	`Set` `instMembership`	`Nontrivial`	—	`Nontrivial.exists_ne` `nontrivial_of_exists_ne`
`nontrivial_iff_ne_singleton` 📖	mathematical	`Set` `instMembership`	`Nontrivial`	—	`Nontrivial.ne_singleton` `eq_singleton_or_nontrivial`
`nontrivial_iff_pair_subset` 📖	mathematical	—	`Nontrivial` `Set` `instHasSubset` `instInsert` `instSingletonSet`	—	`Nontrivial.pair_subset` `nontrivial_of_pair_subset`
`nontrivial_mono` 📖	mathematical	`Set` `instHasSubset`	`Nontrivial` `Elem`	—	`Nontrivial.coe_sort` `Nontrivial.mono` `nontrivial_coe_sort`
`nontrivial_of_exists_lt` 📖	mathematical	`Set` `instMembership` `Preorder.toLT`	`Nontrivial`	—	`nontrivial_of_lt`
`nontrivial_of_exists_ne` 📖	mathematical	`Set` `instMembership`	`Nontrivial`	—	—
`nontrivial_of_lt` 📖	mathematical	`Set` `instMembership` `Preorder.toLT`	`Nontrivial`	—	`ne_of_lt`
`nontrivial_of_mem_mem_ne` 📖	mathematical	`Set` `instMembership`	`Nontrivial`	—	—
`nontrivial_of_nontrivial` 📖	mathematical	`Nontrivial`	`Nontrivial`	—	—
`nontrivial_of_nontrivial_coe` 📖	mathematical	—	`Nontrivial`	—	`nontrivial_of_nontrivial` `nontrivial_coe_sort`
`nontrivial_of_pair_subset` 📖	mathematical	`Set` `instHasSubset` `instInsert` `instSingletonSet`	`Nontrivial`	—	`Nontrivial.mono` `nontrivial_pair`
`nontrivial_of_univ_nontrivial` 📖	mathematical	`Nontrivial` `univ`	`Nontrivial`	—	—
`nontrivial_pair` 📖	mathematical	—	`Nontrivial` `Set` `instInsert` `instSingletonSet`	—	`mem_insert` `mem_insert_of_mem` `mem_singleton`
`nontrivial_univ` 📖	mathematical	—	`Nontrivial` `univ`	—	`exists_pair_ne` `mem_univ`
`nontrivial_univ_iff` 📖	mathematical	—	`Nontrivial` `univ` `Nontrivial`	—	`nontrivial_of_univ_nontrivial` `nontrivial_univ`
`not_nontrivial_empty` 📖	mathematical	—	`Nontrivial` `Set` `instEmptyCollection`	—	`Nontrivial.ne_empty`
`not_nontrivial_iff` 📖	mathematical	—	`Nontrivial` `Subsingleton`	—	`Iff.not_left` `not_subsingleton_iff`
`not_nontrivial_singleton` 📖	mathematical	—	`Nontrivial` `Set` `instSingletonSet`	—	`nontrivial_iff_exists_ne` `mem_singleton` `mem_singleton_iff`
`not_subsingleton_iff` 📖	mathematical	—	`Subsingleton` `Nontrivial`	—	—
`singleton_ne_univ` 📖	—	—	—	—	`Nontrivial.not_subset_singleton` `nontrivial_univ` `Eq.superset` `instReflSubset`
`singleton_ssubset_univ` 📖	mathematical	—	`Set` `instHasSSubset` `instSingletonSet` `univ`	—	`ssubset_univ_iff` `singleton_ne_univ`
`strictAntiOn_singleton` 📖	mathematical	—	`StrictAntiOn` `Set` `instSingletonSet`	—	`Subsingleton.strictAntiOn` `subsingleton_singleton`
`strictMonoOn_singleton` 📖	mathematical	—	`StrictMonoOn` `Set` `instSingletonSet`	—	`Subsingleton.strictMonoOn` `subsingleton_singleton`
`subsingleton_coe` 📖	mathematical	—	`Elem` `Subsingleton`	—	`SetCoe.ext_iff` `SetCoe.ext`
`subsingleton_coe_of_subsingleton` 📖	mathematical	—	`Elem`	—	`subsingleton_coe` `subsingleton_of_subsingleton`
`subsingleton_empty` 📖	mathematical	—	`Subsingleton` `Set` `instEmptyCollection`	—	—
`subsingleton_iff_singleton` 📖	mathematical	`Set` `instMembership`	`Subsingleton` `instSingletonSet`	—	`Subsingleton.eq_singleton_of_mem` `subsingleton_singleton`
`subsingleton_isBot` 📖	mathematical	—	`Subsingleton` `setOf` `IsBot` `Preorder.toLE` `PartialOrder.toPreorder`	—	`IsMin.eq_of_ge` `IsBot.isMin`
`subsingleton_isTop` 📖	mathematical	—	`Subsingleton` `setOf` `IsTop` `Preorder.toLE` `PartialOrder.toPreorder`	—	`IsMax.eq_of_le` `IsTop.isMax`
`subsingleton_of_forall_eq` 📖	mathematical	—	`Subsingleton`	—	—
`subsingleton_of_subset_singleton` 📖	mathematical	`Set` `instHasSubset` `instSingletonSet`	`Subsingleton`	—	`Subsingleton.anti` `subsingleton_singleton`
`subsingleton_of_subsingleton` 📖	mathematical	—	`Subsingleton`	—	`Subsingleton.anti` `subsingleton_univ` `subset_univ`
`subsingleton_of_subsingleton_inter_left` 📖	—	`Subsingleton` `Set` `instUnion`	—	—	—
`subsingleton_of_subsingleton_inter_right` 📖	—	`Subsingleton` `Set` `instUnion`	—	—	—
`subsingleton_of_univ_subsingleton` 📖	—	`Subsingleton` `univ`	—	—	`mem_univ`
`subsingleton_or_nontrivial` 📖	mathematical	—	`Subsingleton` `Nontrivial`	—	—
`subsingleton_singleton` 📖	mathematical	—	`Subsingleton` `Set` `instSingletonSet`	—	`eq_of_mem_singleton`
`subsingleton_univ` 📖	mathematical	—	`Subsingleton` `univ`	—	—
`subsingleton_univ_iff` 📖	mathematical	—	`Subsingleton` `univ`	—	`subsingleton_of_univ_subsingleton` `subsingleton_univ`
`univ_eq_true_false` 📖	mathematical	—	`univ` `Set` `instInsert` `instSingletonSet`	—	`eq_univ_of_forall` `mem_insert_iff` `mem_singleton_iff`
`univ_set_eq_singleton_empty_iff` 📖	mathematical	—	`univ` `Set` `instSingletonSet` `instEmptyCollection` `IsEmpty`	—	`univ_set_of_isEmpty`
`univ_set_of_isEmpty` 📖	mathematical	—	`univ` `Set` `instSingletonSet` `instEmptyCollection`	—	`subset_antisymm` `instAntisymmSubset` `eq_empty_of_isEmpty` `instIsEmptySubtype`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eq_singleton_or_nontrivial` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instSingletonSet` `Set.Nontrivial`	—	`Set.eq_singleton_or_nontrivial`

Set.Nontrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`choose_fst_mem` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instMembership` `choose`	—	—
`choose_fst_ne_choose_snd` 📖	—	`Set.Nontrivial`	—	—	—
`choose_snd_mem` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instMembership` `choose`	—	—
`coe_sort` 📖	mathematical	`Set.Nontrivial`	`Nontrivial` `Set.Elem`	—	`Set.nontrivial_coe_sort`
`exists_lt` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`lt_or_gt_of_ne`
`exists_ne` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instMembership`	—	`Mathlib.Tactic.Push.not_and_eq`
`mono` 📖	—	`Set.Nontrivial` `Set` `Set.instHasSubset`	—	—	—
`ne_empty` 📖	—	`Set.Nontrivial`	—	—	`Set.Nonempty.ne_empty` `nonempty`
`ne_singleton` 📖	—	`Set.Nontrivial`	—	—	`Set.not_nontrivial_singleton`
`nonempty` 📖	mathematical	`Set.Nontrivial`	`Set.Nonempty`	—	—
`not_subset_empty` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instHasSubset` `Set.instEmptyCollection`	—	`Set.Nonempty.not_subset_empty` `nonempty`
`not_subset_singleton` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instHasSubset` `Set.instSingletonSet`	—	`Set.subset_singleton_iff_eq` `ne_empty` `ne_singleton`
`not_subsingleton` 📖	mathematical	`Set.Nontrivial`	`Set.Subsingleton`	—	`Set.not_subsingleton_iff`
`pair_subset` 📖	mathematical	`Set.Nontrivial`	`Set` `Set.instHasSubset` `Set.instInsert` `Set.instSingletonSet`	—	`Set.insert_subset` `Set.singleton_subset_iff`

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`anti` 📖	—	`Set.Subsingleton` `Set` `Set.instHasSubset`	—	—	—
`antitoneOn` 📖	mathematical	`Set.Subsingleton`	`AntitoneOn`	—	`Eq.le`
`coe_sort` 📖	mathematical	`Set.Subsingleton`	`Set.Elem`	—	`Set.subsingleton_coe`
`denselyOrdered` 📖	mathematical	`Set.Subsingleton`	`DenselyOrdered` `Set.Elem` `Set` `Set.instMembership`	—	`Set.subsingleton_coe` `LT.lt.trans_eq`
`eq_empty_or_singleton` 📖	mathematical	`Set.Subsingleton`	`Set` `Set.instEmptyCollection` `Set.instSingletonSet`	—	`Set.eq_empty_or_nonempty` `eq_singleton_of_mem`
`eq_singleton_of_mem` 📖	mathematical	`Set.Subsingleton` `Set` `Set.instMembership`	`Set.instSingletonSet`	—	`Set.ext` `Set.mem_singleton` `Set.eq_of_mem_singleton`
`induction_on` 📖	—	`Set.Subsingleton` `Set` `Set.instEmptyCollection` `Set.instSingletonSet`	—	—	`eq_empty_or_singleton`
`inter_singleton` 📖	mathematical	—	`Set.Subsingleton` `Set` `Set.instInter` `Set.instSingletonSet`	—	`Set.subsingleton_of_subset_singleton` `Set.inter_subset_right`
`monotoneOn` 📖	mathematical	`Set.Subsingleton`	`MonotoneOn`	—	`Eq.le`
`not_nontrivial` 📖	mathematical	`Set.Subsingleton`	`Set.Nontrivial`	—	`Set.not_nontrivial_iff`
`singleton_inter` 📖	mathematical	—	`Set.Subsingleton` `Set` `Set.instInter` `Set.instSingletonSet`	—	`Set.subsingleton_of_subset_singleton` `Set.inter_subset_left`
`strictAntiOn` 📖	mathematical	`Set.Subsingleton`	`StrictAntiOn`	—	`LT.lt.ne`
`strictMonoOn` 📖	mathematical	`Set.Subsingleton`	`StrictMonoOn`	—	`LT.lt.ne`

---

← Back to Index