setOf stuff

@[simp]

theorem Set.mem_setOf_iff {α : Type u_1} {p : α → Prop} {x : α} : x ∈ {y : α | p y} ↔ p x

theorem Set.mem_setOf_of {α : Type u_1} {p : α → Prop} {x : α} (h : p x) : x ∈ {y : α | p y}

theorem Set.of_mem_setOf {α : Type u_1} {p : α → Prop} {x : α} (h : x ∈ {y : α | p y}) : p x

subsets

@[simp]

theorem Set.subset_refl {α : Type u_1} (x : Set α) : x ⊆ x

theorem Set.subset_rfl {α : Type u_1} {x : Set α} : x ⊆ x

theorem Set.subset_trans {α : Type u_1} {x y z : Set α} (h : x ⊆ y) (h' : y ⊆ z) : x ⊆ z

theorem Set.subset_of_eq {α : Type u_1} {x y : Set α} (h : x = y) : x ⊆ y

instance Set.instTransSubset {α : Type u_1} : Trans (fun (x y : Set α) => x ⊆ y) (fun (x y : Set α) => x ⊆ y) fun (x y : Set α) => x ⊆ y

Equations

• Set.instTransSubset = { trans := ⋯ }

theorem Set.subset_antisym {α : Type u_1} {x y : Set α} (h : x ⊆ y) (h' : y ⊆ x) : x = y

theorem Set.eq_iff_subset_subset {α : Type u_1} {x y : Set α} : x = y ↔ x ⊆ y ∧ y ⊆ x

@[simp]

theorem Set.setOf_subset_iff {α : Type u_1} {p : α → Prop} {x : Set α} : {y : α | p y} ⊆ x ↔ ∀ (a : α), p a → a ∈ x

@[simp]

theorem Set.subset_setOf_iff {α : Type u_1} {p : α → Prop} {x : Set α} : x ⊆ {y : α | p y} ↔ ∀ (a : α), a ∈ x → p a

@[simp]

theorem Set.setOf_subset_setOf_iff {α : Type u_1} {p q : α → Prop} : {y : α | p y} ⊆ {y : α | q y} ↔ ∀ (a : α), p a → q a

@[simp]

theorem Set.setOf_eq_setOf_iff {α : Type u_1} {p q : α → Prop} : {y : α | p y} = {y : α | q y} ↔ ∀ (a : α), p a ↔ q a

simp lemmas

@[simp]

theorem Set.mem_univ {α : Type u_1} {a : α} : a ∈ Set.univ

@[simp]

theorem Set.subset_univ {α : Type u_1} {x : Set α} : x ⊆ Set.univ

@[simp]

theorem Set.not_mem_empty {α : Type u_1} {a : α} : ¬a ∈ ∅

@[simp]

theorem Set.empty_subset {α : Type u_1} {x : Set α} : ∅ ⊆ x

@[simp]

theorem Set.mem_singleton_iff {α : Type u_1} {a b : α} : a ∈ {b} ↔ a = b

theorem Set.subset_empty_iff {α : Type u_1} {x : Set α} : x ⊆ ∅ ↔ x = ∅

theorem Set.univ_subset_iff {α : Type u_1} {x : Set α} : Set.univ ⊆ x ↔ x = Set.univ

elements of operations

@[simp]

theorem Set.mem_sdiff_iff {α : Type u_1} {x y : Set α} {a : α} : a ∈ x \ y ↔ a ∈ x ∧ ¬a ∈ y

@[simp]

theorem Set.mem_compl_iff {α : Type u_1} {x : Set α} {a : α} : a ∈ xᶜ ↔ ¬a ∈ x

@[simp]

theorem Set.mem_powerset_iff {α : Type u_1} {x a : Set α} : a ∈ 𝒫 x ↔ a ⊆ x

complement lemmas

@[simp]

theorem Set.compl_compl {α : Type u_1} {x : Set α} : xᶜᶜ = x

@[simp]

theorem Set.sdiff_univ_eq_compl {α : Type u_1} {x : Set α} : Set.univ \ x = xᶜ

theorem Set.subset_compl_iff_subset_compl {α : Type u_1} {x y : Set α} : x ⊆ yᶜ ↔ y ⊆ xᶜ

theorem Set.compl_subset_iff_compl_subset {α : Type u_1} {x y : Set α} : xᶜ ⊆ y ↔ yᶜ ⊆ x

misc

@[simp]

theorem Set.subset_singleton_iff {α : Type u_1} {x : Set α} {a : α} : x ⊆ {a} ↔ x = {a} ∨ x = ∅

@[simp]

theorem Set.empty_not_nonempty {α : Type u_1} : ¬∅.Nonempty

sets of products

def Set.prod {α : Type u_1} {β : Type u_2} (x : Set α) (y : Set β) : Set (α × β)

Equations

• x.prod y = {a : α × β | a.fst ∈ x ∧ a.snd ∈ y}

@[simp]

theorem Set.mem_prod_iff {α : Type u_1} {β : Type u_2} {a : α} {b : β} {x : Set α} {y : Set β} : (a, b) ∈ x.prod y ↔ a ∈ x ∧ b ∈ y

@[simp]

theorem Set.prod_subset_prod_nonempty_iff {α : Type u_1} {β : Type u_2} {x x' : Set α} {y y' : Set β} (hx : x.Nonempty) (hy : y.Nonempty) : x.prod y ⊆ x'.prod y' ↔ x ⊆ x' ∧ y ⊆ y'

for nonempty sets, products are subsets of another iff the factors are

@[simp]

theorem Set.prod_empty_iff {α : Type u_1} {β : Type u_2} {x : Set α} {y : Set β} : (x.prod y).Nonempty ↔ x.Nonempty ∧ y.Nonempty

@[simp]

theorem Set.prod_univ_univ {α : Type u_1} {β : Type u_2} : Set.univ.prod Set.univ = Set.univ

nonempty equivalences

theorem Set.nonempty_iff_neq_empty {α : Type u_1} {x : Set α} : x.Nonempty ↔ x ≠ ∅

@[simp]

theorem Set.singleton_neq_empty {α : Type u_1} {a : α} : {a} ≠ ∅

@[simp]

theorem Set.mem_pair_iff {α : Type u_1} {a b c : α} : c ∈ {a, b} ↔ c = a ∨ c = b

instance Set.instUniqueSubtypeMemSingleton {α : Type u_1} {a : α} : Unique ↥{a}

Equations

• Set.instUniqueSubtypeMemSingleton = { default := ⟨a, ⋯⟩, uniq := ⋯ }

theorem Set.cases_of_empty {α : Type u_1} {p : Set α → Prop} (h : p ∅) (h' : ∀ (a : Set α), a.Nonempty → p a) (a : Set α) : p a