Insert

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

Statistics

Metric	Count
Definitions `decidableSingleton`, `subtypeInsertEquivOption`, `uniqueSingleton`, `Insert`	4
Theorems `ssubset_of_mem_notMem`, `compl_singleton`, `eq_one`, `eq_zero`, `subset_pair_iff_eq`, `subset_singleton_iff`, `default_coe_singleton`, `disjoint_insert_left`, `disjoint_insert_right`, `disjoint_singleton`, `disjoint_singleton_left`, `disjoint_singleton_right`, `empty_ne_singleton`, `empty_ssubset_singleton`, `eq_empty_of_ssubset_singleton`, `eq_of_mem_insert_of_notMem`, `eq_of_mem_singleton`, `eq_of_nonempty_of_subsingleton`, `eq_of_nonempty_of_subsingleton'`, `eq_or_mem_of_mem_insert`, `eq_singleton_iff_nonempty_unique_mem`, `eq_singleton_iff_unique_mem`, `exists_mem_insert`, `forall_insert_of_forall`, `forall_mem_insert`, `forall_of_forall_insert`, `insert_comm`, `insert_def`, `insert_diff_eq_singleton`, `insert_eq`, `insert_eq_of_mem`, `insert_eq_self`, `insert_idem`, `insert_inj`, `insert_inter_distrib`, `insert_inter_of_mem`, `insert_inter_of_notMem`, `insert_ne_self`, `insert_nonempty`, `insert_subset`, `insert_subset_iff`, `insert_subset_insert`, `insert_subset_insert_iff`, `insert_union`, `insert_union_distrib`, `instLawfulSingleton`, `instNonemptyElemInsert`, `inter_insert_of_mem`, `inter_insert_of_notMem`, `inter_singleton_eq_empty`, `inter_singleton_nonempty`, `inter_singleton_of_mem`, `inter_singleton_of_notMem`, `mem_insert`, `mem_insert_iff`, `mem_insert_of_mem`, `mem_of_mem_insert_of_ne`, `mem_singleton`, `mem_singleton_iff`, `mem_singleton_of_eq`, `ne_insert_of_notMem`, `notMem_singleton_empty`, `notMem_singleton_iff`, `pair_comm`, `pair_eq_pair_iff`, `pair_eq_singleton`, `pair_subset`, `pair_subset_iff`, `powerset_singleton`, `preimage_fst_singleton_eq_range`, `preimage_snd_singleton_eq_range`, `setOf_eq_eq_singleton`, `setOf_eq_eq_singleton'`, `setOf_mem_list_eq_replicate`, `setOf_mem_list_eq_singleton_of_nodup`, `set_compr_eq_eq_singleton`, `singleton_def`, `singleton_eq_singleton_iff`, `singleton_injective`, `singleton_inter_eq_empty`, `singleton_inter_nonempty`, `singleton_inter_of_mem`, `singleton_inter_of_notMem`, `singleton_ne_empty`, `singleton_nonempty`, `singleton_subset_iff`, `singleton_subset_singleton`, `singleton_union`, `ssubset_iff_insert`, `ssubset_insert`, `ssubset_singleton_iff`, `subset_insert`, `subset_insert_iff_of_notMem`, `subset_pair_iff`, `subset_pair_iff_eq`, `subset_singleton_iff`, `subset_singleton_iff_eq`, `union_insert`, `union_singleton`	99
Total	103

HasSubset.Subset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ssubset_of_mem_notMem` 📖	mathematical	`Set` `Set.instHasSubset` `Set.instMembership`	`Set.instHasSSubset`	—	—

Prop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compl_singleton` 📖	mathematical	—	`Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	—	`Set.ext` `not_iff`

Set

Definitions

Name	Category	Theorems
`decidableSingleton` 📖	CompOp	2 math math: `DFinsupp.piecewise_single_erase`, `SimpleGraph.card_edgeFinset_induce_compl_singleton`
`subtypeInsertEquivOption` 📖	CompOp	—
`uniqueSingleton` 📖	CompOp	3 math math: `EuclideanGeometry.orthogonalProjection_affineSpan_singleton`, `default_coe_singleton`, `AffineSubspace.signedInfDist_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`default_coe_singleton` 📖	mathematical	—	`Elem` `Set` `instSingletonSet` `Unique.instInhabited` `uniqueSingleton` `instMembership`	—	—
`disjoint_insert_left` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instInsert` `instMembership`	—	—
`disjoint_insert_right` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instInsert` `instMembership`	—	`disjoint_comm` `disjoint_insert_left`
`disjoint_singleton` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instSingletonSet`	—	—
`disjoint_singleton_left` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instSingletonSet` `instMembership`	—	—
`disjoint_singleton_right` 📖	mathematical	—	`Disjoint` `Set` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLattice` `BoundedOrder.toOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `instBoundedOrder` `instSingletonSet` `instMembership`	—	`disjoint_comm` `disjoint_singleton_left`
`empty_ne_singleton` 📖	—	—	—	—	`singleton_ne_empty`
`empty_ssubset_singleton` 📖	mathematical	—	`Set` `instHasSSubset` `instEmptyCollection` `instSingletonSet`	—	`Nonempty.empty_ssubset` `singleton_nonempty`
`eq_empty_of_ssubset_singleton` 📖	mathematical	`Set` `instHasSSubset` `instSingletonSet`	`instEmptyCollection`	—	`ssubset_singleton_iff`
`eq_of_mem_insert_of_notMem` 📖	—	`Set` `instMembership` `instInsert`	—	—	—
`eq_of_mem_singleton` 📖	—	`Set` `instMembership` `instSingletonSet`	—	—	—
`eq_of_nonempty_of_subsingleton` 📖	—	—	—	—	`Nonempty.eq_univ` `Nonempty.of_subtype`
`eq_of_nonempty_of_subsingleton'` 📖	—	`Nonempty`	—	—	`Nonempty.to_subtype` `eq_of_nonempty_of_subsingleton`
`eq_or_mem_of_mem_insert` 📖	—	`Set` `instMembership` `instInsert`	—	—	—
`eq_singleton_iff_nonempty_unique_mem` 📖	mathematical	—	`Set` `instSingletonSet` `Nonempty`	—	`eq_singleton_iff_unique_mem`
`eq_singleton_iff_unique_mem` 📖	mathematical	—	`Set` `instSingletonSet` `instMembership`	—	`Subset.antisymm_iff` `singleton_subset_iff`
`exists_mem_insert` 📖	mathematical	—	`Set` `instMembership` `instInsert`	—	—
`forall_insert_of_forall` 📖	—	`Set` `instMembership` `instInsert`	—	—	—
`forall_mem_insert` 📖	—	—	—	—	—
`forall_of_forall_insert` 📖	—	`Set` `instMembership`	—	—	—
`insert_comm` 📖	mathematical	—	`Set` `instInsert`	—	—
`insert_def` 📖	mathematical	—	`Set` `instInsert` `setOf` `instMembership`	—	—
`insert_diff_eq_singleton` 📖	mathematical	`Set` `instMembership`	`instSDiff` `instInsert` `instSingletonSet`	—	—
`insert_eq` 📖	mathematical	—	`Set` `instInsert` `instUnion` `instSingletonSet`	—	—
`insert_eq_of_mem` 📖	mathematical	`Set` `instMembership`	`instInsert`	—	—
`insert_eq_self` 📖	mathematical	—	`Set` `instInsert` `instMembership`	—	—
`insert_idem` 📖	mathematical	—	`Set` `instInsert`	—	—
`insert_inj` 📖	mathematical	`Set` `instMembership`	`instInsert`	—	`eq_of_mem_insert_of_notMem` `mem_insert`
`insert_inter_distrib` 📖	mathematical	—	`Set` `instInsert` `instInter`	—	—
`insert_inter_of_mem` 📖	mathematical	`Set` `instMembership`	`instInter` `instInsert`	—	—
`insert_inter_of_notMem` 📖	mathematical	`Set` `instMembership`	`instInter` `instInsert`	—	—
`insert_ne_self` 📖	mathematical	—	`Set` `instMembership`	—	—
`insert_nonempty` 📖	mathematical	—	`Nonempty` `Set` `instInsert`	—	`mem_insert`
`insert_subset` 📖	mathematical	`Set` `instMembership` `instHasSubset`	`instInsert`	—	—
`insert_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `instInsert` `instMembership`	—	—
`insert_subset_insert` 📖	mathematical	`Set` `instHasSubset`	`instInsert`	—	—
`insert_subset_insert_iff` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `instInsert`	—	—
`insert_union` 📖	mathematical	—	`Set` `instUnion` `instInsert`	—	—
`insert_union_distrib` 📖	mathematical	—	`Set` `instInsert` `instUnion`	—	—
`instLawfulSingleton` 📖	mathematical	—	`Set` `instEmptyCollection` `instInsert` `instSingletonSet`	—	`ext`
`instNonemptyElemInsert` 📖	mathematical	—	`Elem` `Set` `instInsert`	—	`Nonempty.to_subtype` `insert_nonempty`
`inter_insert_of_mem` 📖	mathematical	`Set` `instMembership`	`instInter` `instInsert`	—	—
`inter_insert_of_notMem` 📖	mathematical	`Set` `instMembership`	`instInter` `instInsert`	—	—
`inter_singleton_eq_empty` 📖	mathematical	—	`Set` `instInter` `instSingletonSet` `instEmptyCollection` `instMembership`	—	`inter_comm` `singleton_inter_eq_empty`
`inter_singleton_nonempty` 📖	mathematical	—	`Nonempty` `Set` `instInter` `instSingletonSet` `instMembership`	—	`inter_comm` `singleton_inter_nonempty`
`inter_singleton_of_mem` 📖	mathematical	`Set` `instMembership`	`instInter` `instSingletonSet`	—	—
`inter_singleton_of_notMem` 📖	mathematical	`Set` `instMembership`	`instInter` `instSingletonSet` `instEmptyCollection`	—	`inter_singleton_eq_empty`
`mem_insert` 📖	mathematical	—	`Set` `instMembership` `instInsert`	—	—
`mem_insert_iff` 📖	mathematical	—	`Set` `instMembership` `instInsert`	—	—
`mem_insert_of_mem` 📖	mathematical	`Set` `instMembership`	`instInsert`	—	—
`mem_of_mem_insert_of_ne` 📖	—	`Set` `instMembership` `instInsert`	—	—	—
`mem_singleton` 📖	mathematical	—	`Set` `instMembership` `instSingletonSet`	—	—
`mem_singleton_iff` 📖	mathematical	—	`Set` `instMembership` `instSingletonSet`	—	—
`mem_singleton_of_eq` 📖	mathematical	—	`Set` `instMembership` `instSingletonSet`	—	—
`ne_insert_of_notMem` 📖	—	`Set` `instMembership`	—	—	—
`notMem_singleton_empty` 📖	mathematical	—	`Set` `instMembership` `instSingletonSet` `instEmptyCollection` `Nonempty`	—	`nonempty_iff_ne_empty`
`notMem_singleton_iff` 📖	mathematical	—	`Set` `instMembership` `instSingletonSet`	—	—
`pair_comm` 📖	mathematical	—	`Set` `instInsert` `instSingletonSet`	—	`union_comm`
`pair_eq_pair_iff` 📖	mathematical	—	`Set` `instInsert` `instSingletonSet`	—	`instReflSubset` `instAntisymmSubset`
`pair_eq_singleton` 📖	mathematical	—	`Set` `instInsert` `instSingletonSet`	—	`union_self`
`pair_subset` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `instInsert` `instSingletonSet`	—	`pair_subset_iff`
`pair_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `instInsert` `instSingletonSet` `instMembership`	—	—
`powerset_singleton` 📖	mathematical	—	`powerset` `Set` `instSingletonSet` `instInsert` `instEmptyCollection`	—	—
`preimage_fst_singleton_eq_range` 📖	mathematical	—	`preimage` `Set` `instSingletonSet` `range`	—	—
`preimage_snd_singleton_eq_range` 📖	mathematical	—	`preimage` `Set` `instSingletonSet` `range`	—	—
`setOf_eq_eq_singleton` 📖	mathematical	—	`setOf` `Set` `instSingletonSet`	—	—
`setOf_eq_eq_singleton'` 📖	mathematical	—	`setOf` `Set` `instSingletonSet`	—	`ext`
`setOf_mem_list_eq_replicate` 📖	mathematical	—	`setOf` `Set` `instSingletonSet`	—	—
`setOf_mem_list_eq_singleton_of_nodup` 📖	mathematical	—	`setOf` `Set` `instSingletonSet`	—	`setOf_mem_list_eq_replicate`
`set_compr_eq_eq_singleton` 📖	mathematical	—	`setOf` `Set` `instSingletonSet`	—	—
`singleton_def` 📖	mathematical	—	`Set` `instSingletonSet` `instInsert` `instEmptyCollection`	—	`instLawfulSingleton`
`singleton_eq_singleton_iff` 📖	mathematical	—	`Set` `instSingletonSet`	—	`ext_iff` `eq_iff_eq_cancel_left`
`singleton_injective` 📖	mathematical	—	`Set` `instSingletonSet`	—	`singleton_eq_singleton_iff`
`singleton_inter_eq_empty` 📖	mathematical	—	`Set` `instInter` `instSingletonSet` `instEmptyCollection` `instMembership`	—	`not_nonempty_iff_eq_empty` `Iff.not` `singleton_inter_nonempty`
`singleton_inter_nonempty` 📖	mathematical	—	`Nonempty` `Set` `instInter` `instSingletonSet` `instMembership`	—	—
`singleton_inter_of_mem` 📖	mathematical	`Set` `instMembership`	`instInter` `instSingletonSet`	—	—
`singleton_inter_of_notMem` 📖	mathematical	`Set` `instMembership`	`instInter` `instSingletonSet` `instEmptyCollection`	—	`singleton_inter_eq_empty`
`singleton_ne_empty` 📖	—	—	—	—	`Nonempty.ne_empty` `singleton_nonempty`
`singleton_nonempty` 📖	mathematical	—	`Nonempty` `Set` `instSingletonSet`	—	—
`singleton_subset_iff` 📖	mathematical	—	`Set` `instHasSubset` `instSingletonSet` `instMembership`	—	—
`singleton_subset_singleton` 📖	mathematical	—	`Set` `instHasSubset` `instSingletonSet`	—	—
`singleton_union` 📖	mathematical	—	`Set` `instUnion` `instSingletonSet` `instInsert`	—	—
`ssubset_iff_insert` 📖	mathematical	—	`Set` `instHasSSubset` `instMembership` `instHasSubset` `instInsert`	—	—
`ssubset_insert` 📖	mathematical	`Set` `instMembership`	`instHasSSubset` `instInsert`	—	—
`ssubset_singleton_iff` 📖	mathematical	—	`Set` `instHasSSubset` `instSingletonSet` `instEmptyCollection`	—	`ssubset_iff_subset_ne` `instIsNonstrictStrictOrderSubsetSSubset` `instAntisymmSubset` `subset_singleton_iff_eq` `empty_ne_singleton`
`subset_insert` 📖	mathematical	—	`Set` `instHasSubset` `instInsert`	—	—
`subset_insert_iff_of_notMem` 📖	mathematical	`Set` `instMembership`	`instHasSubset` `instInsert`	—	—
`subset_pair_iff` 📖	mathematical	—	`Set` `instHasSubset` `instInsert` `instSingletonSet`	—	—
`subset_pair_iff_eq` 📖	mathematical	—	`Set` `instHasSubset` `instInsert` `instSingletonSet` `instEmptyCollection`	—	—
`subset_singleton_iff` 📖	mathematical	—	`Set` `instHasSubset` `instSingletonSet`	—	—
`subset_singleton_iff_eq` 📖	mathematical	—	`Set` `instHasSubset` `instSingletonSet` `instEmptyCollection`	—	—
`union_insert` 📖	mathematical	—	`Set` `instUnion` `instInsert`	—	—
`union_singleton` 📖	mathematical	—	`Set` `instUnion` `instSingletonSet` `instInsert`	—	`union_comm`

Set.Nonempty

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_one` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instSingletonSet`	—	`Set.eq_of_nonempty_of_subsingleton'`
`eq_zero` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instSingletonSet`	—	`Set.eq_of_nonempty_of_subsingleton'`
`subset_pair_iff_eq` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instHasSubset` `Set.instInsert` `Set.instSingletonSet`	—	`Set.subset_pair_iff_eq` `ne_empty`
`subset_singleton_iff` 📖	mathematical	`Set.Nonempty`	`Set` `Set.instHasSubset` `Set.instSingletonSet`	—	`Set.subset_singleton_iff_eq` `ne_empty`

ZFSet

Definitions

Name	Category	Theorems
`Insert` 📖	CompOp	—

---

← Back to Index