Lemmas about insertion, singleton, and pairs #
This file provides extra lemmas about insert
, singleton
, and pair
.
Tags #
insert, singleton
Set coercion to a type #
Lemmas about insert
#
insert α s
is the set {α} ∪ s
.
@[deprecated Set.eq_of_mem_insert_of_notMem (since := "2025-05-23")]
Alias of Set.eq_of_mem_insert_of_notMem
.
@[deprecated Set.ne_insert_of_notMem (since := "2025-05-23")]
Alias of Set.ne_insert_of_notMem
.
@[deprecated Set.subset_insert_iff_of_notMem (since := "2025-05-23")]
Alias of Set.subset_insert_iff_of_notMem
.
@[deprecated HasSubset.Subset.ssubset_of_mem_notMem (since := "2025-05-23")]
theorem
HasSubset.Subset.ssubset_of_mem_not_mem
{α : Type u}
{s t : Set α}
{a : α}
(hst : s ⊆ t)
(hat : a ∈ t)
(has : a ∉ s)
:
Alias of HasSubset.Subset.ssubset_of_mem_notMem
.
Inserting an element to a set is equivalent to the option type.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Lemmas about singletons #
@[deprecated Set.notMem_singleton_iff (since := "2025-05-23")]
Alias of Set.notMem_singleton_iff
.
Alias of the reverse direction of Set.singleton_subset_singleton
.
@[deprecated Set.notMem_singleton_empty (since := "2025-05-24")]
Alias of Set.notMem_singleton_empty
.
theorem
Set.eq_of_nonempty_of_subsingleton
{α : Type u_1}
[Subsingleton α]
(s t : Set α)
[Nonempty ↑s]
[Nonempty ↑t]
:
theorem
Set.eq_of_nonempty_of_subsingleton'
{α : Type u_1}
[Subsingleton α]
{s : Set α}
(t : Set α)
(hs : s.Nonempty)
[Nonempty ↑t]
:
Disjointness #
Lemmas about complement #
@[simp]
Lemmas about set difference #
@[deprecated Set.diff_insert_of_notMem (since := "2025-05-23")]
Alias of Set.diff_insert_of_notMem
.
@[deprecated Set.insert_diff_self_of_notMem (since := "2025-05-23")]
Alias of Set.insert_diff_self_of_notMem
.
@[deprecated Set.inter_insert_of_notMem (since := "2025-05-23")]
Alias of Set.inter_insert_of_notMem
.
@[deprecated Set.insert_inter_of_notMem (since := "2025-05-23")]
Alias of Set.insert_inter_of_notMem
.
Lemmas about pairs #
Powerset #
Lemmas about inclusion
, the injection of subtypes induced by ⊆
#
Decidability instances for sets #
Equations
- Set.decidableSingleton a b = inferInstanceAs (Decidable (a = b))