Sets

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

theorem Disjoint.ni_right_of_in_left {α : Type u_1} {X Y : Set α} {a : α} (hXY : X ⫗ Y) (ha : a ∈ X) : a ∉ Y

theorem Disjoint.ni_left_of_in_right {α : Type u_1} {X Y : Set α} {a : α} (hXY : X ⫗ Y) (ha : a ∈ Y) : a ∉ X

theorem in_left_of_in_union_of_ni_right {α : Type u_1} {X Y : Set α} {a : α} (haXY : a ∈ X ∪ Y) (haY : a ∉ Y) : a ∈ X

theorem in_right_of_in_union_of_ni_left {α : Type u_1} {X Y : Set α} {a : α} (haXY : a ∈ X ∪ Y) (haX : a ∉ X) : a ∈ Y

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

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

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

theorem union_disjoint_union_iff {α : Type u_1} (A₁ A₂ B₁ B₂ : Set α) : A₁ ∪ A₂ ⫗ B₁ ∪ B₂ ↔ (A₁ ⫗ B₁ ∧ A₂ ⫗ B₁) ∧ A₁ ⫗ B₂ ∧ A₂ ⫗ B₂

theorem union_disjoint_union_aux {α : Type u_1} {A B C D : Set α} (hAB : A ⫗ B) (hCD : C ⫗ D) (hCB : C ⫗ B) (hAD : A ⫗ D) : A ∪ C ⫗ B ∪ D

theorem union_disjoint_union {α : Type u_1} {A B C D : Set α} (hAB : A ⫗ B) (hCD : C ⫗ D) (hAD : A ⫗ D) (hBC : B ⫗ C) : A ∪ C ⫗ B ∪ D

theorem Subtype.subst_elem {α : Type u_1} {X Y : Set α} (x : ↑X) (hXY : X = Y) : ↑(hXY ▸ x) = ↑x

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

def HasSubset.Subset.equiv {α : Type u_1} {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 u_1} {β : Type u_2} [Zero β] {f : α → β} {S : Set α} (hS : Finite ↑S) (hfS : f.support = S) : ↑(Finsupp.ofSupportFinite f ⋯).support = S

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