Sets

This file provides lemmas about sets that are not present in Mathlib.

theorem singleton_inter_in_left {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : a ∈ X

theorem singleton_inter_in_right {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : a ∈ Y

theorem disjoint_of_sdiff_inter {α : Type} (X Y : Set α) : X \ (X ∩ Y) ⫗ Y \ (X ∩ Y)

theorem disjoint_of_sdiff_singleton {α : Type} {X Y : Set α} {a : α} (ha : X ∩ Y = {a}) : X \ {a} ⫗ Y \ {a}

theorem right_eq_right_of_union_eq_union {α : Type} {A₁ A₂ B₁ B₂ : Set α} (hA : A₁ = A₂) (hB₁ : A₁ ⫗ B₁) (hB₂ : A₂ ⫗ B₂) (hAB : A₁ ∪ B₁ = A₂ ∪ B₂) : B₁ = B₂

theorem eq_toFinset_of_toSet_eq {α : Type} {s : Finset α} {S : Set α} [Fintype ↑S] (hsS : ↑s = S) : s = S.toFinset

theorem impossible_nmem_sdiff_triplet {α : Type} {S : Set α} {a b c : α} {e : ↑(S \ {c})} (heS : ↑e ∉ S \ (a ᕃ b ᕃ {c})) (hea : ↑e ≠ a) (heb : ↑e ≠ b) : False

def HasSubset.Subset.equiv {α : Type} {A B : Set α} [(i : α) → Decidable (i ∈ A)] (hAB : A ⊆ B) : ↑A ⊕ ↑(B \ A) ≃ ↑B

Equations

• hAB.equiv = { toFun := fun (x : ↑A ⊕ ↑(B \ A)) => Sum.casesOn x hAB.elem ⋯.elem, invFun := fun (i : ↑B) => if hiA : ↑i ∈ A then ◩⟨↑i, hiA⟩ else ◪⟨↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem ofSupportFinite_support_eq {α β : Type} [Zero β] {f : α → β} {S : Set α} (hS : Finite ↑S) (hfS : f.support = S) : ↑(Finsupp.ofSupportFinite f ⋯).support = S

theorem finset_of_cardinality_between {α β : Type} [Fintype α] [Fintype β] {n : ℕ} (hα : #α < n) (hn : n ≤ #α + #β) : ∃ (b : Finset β), #(α ⊕ { x : β // x ∈ b }) = n ∧ Nonempty { x : β // x ∈ b }