Subsingleton

Defines the predicate Subsingleton s : Prop, saying that s has at most one element.

Also defines Nontrivial s : Prop : the predicate saying that s has at least two distinct elements.

Subsingleton

def Set.Subsingleton {α : Type u} (s : Set α) : Prop

A set s is a Subsingleton if it has at most one element.

Equations

• Set.Subsingleton s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x = y

theorem Set.Subsingleton.anti {α : Type u} {s : Set α} {t : Set α} (ht : Set.Subsingleton t) (hst : s ⊆ t) : Set.Subsingleton s

theorem Set.Subsingleton.eq_singleton_of_mem {α : Type u} {s : Set α} (hs : Set.Subsingleton s) {x : α} (hx : x ∈ s) : s = {x}

@[simp]

theorem Set.subsingleton_empty {α : Type u} : Set.Subsingleton ∅

@[simp]

theorem Set.subsingleton_singleton {α : Type u} {a : α} : Set.Subsingleton {a}

theorem Set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : Set α} (h : s ⊆ {a}) : Set.Subsingleton s

theorem Set.subsingleton_of_forall_eq {α : Type u} {s : Set α} (a : α) (h : ∀ b ∈ s, b = a) : Set.Subsingleton s

theorem Set.subsingleton_iff_singleton {α : Type u} {s : Set α} {x : α} (hx : x ∈ s) : Set.Subsingleton s ↔ s = {x}

theorem Set.Subsingleton.eq_empty_or_singleton {α : Type u} {s : Set α} (hs : Set.Subsingleton s) : s = ∅ ∨ ∃ (x : α), s = {x}

theorem Set.Subsingleton.induction_on {α : Type u} {s : Set α} {p : Set α → Prop} (hs : Set.Subsingleton s) (he : p ∅) (h₁ : ∀ (x : α), p {x}) : p s

theorem Set.subsingleton_univ {α : Type u} [Subsingleton α] : Set.Subsingleton Set.univ

theorem Set.subsingleton_of_univ_subsingleton {α : Type u} (h : Set.Subsingleton Set.univ) : Subsingleton α

@[simp]

theorem Set.subsingleton_univ_iff {α : Type u} : Set.Subsingleton Set.univ ↔ Subsingleton α

theorem Set.subsingleton_of_subsingleton {α : Type u} [Subsingleton α] {s : Set α} : Set.Subsingleton s

theorem Set.subsingleton_isTop (α : Type u_1) [PartialOrder α] : Set.Subsingleton {x : α | IsTop x}

theorem Set.subsingleton_isBot (α : Type u_1) [PartialOrder α] : Set.Subsingleton {x : α | IsBot x}

theorem Set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : Set α} : (∃ (a : α), s = {a}) ↔ Set.Nonempty s ∧ Set.Subsingleton s

@[simp]

theorem Set.subsingleton_coe {α : Type u} (s : Set α) : Subsingleton ↑s ↔ Set.Subsingleton s

s, coerced to a type, is a subsingleton type if and only if s is a subsingleton set.

theorem Set.Subsingleton.coe_sort {α : Type u} {s : Set α} : Set.Subsingleton s → Subsingleton ↑s

instance Set.subsingleton_coe_of_subsingleton {α : Type u} [Subsingleton α] {s : Set α} : Subsingleton ↑s

The coe_sort of a set s in a subsingleton type is a subsingleton. For the corresponding result for Subtype, see subtype.subsingleton.

Equations

• ⋯ = ⋯

Nontrivial

def Set.Nontrivial {α : Type u} (s : Set α) : Prop

A set s is Set.Nontrivial if it has at least two distinct elements.

Equations

• Set.Nontrivial s = ∃ x ∈ s, ∃ y ∈ s, x ≠ y

theorem Set.nontrivial_of_mem_mem_ne {α : Type u} {s : Set α} {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : Set.Nontrivial s

noncomputable def Set.Nontrivial.choose {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : α × α

Extract witnesses from s.nontrivial. This function might be used instead of case analysis on the argument. Note that it makes a proof depend on the classical.choice axiom.

Equations

• Set.Nontrivial.choose hs = (Exists.choose hs, Exists.choose ⋯)

theorem Set.Nontrivial.choose_fst_mem {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : (Set.Nontrivial.choose hs).1 ∈ s

theorem Set.Nontrivial.choose_snd_mem {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : (Set.Nontrivial.choose hs).2 ∈ s

theorem Set.Nontrivial.choose_fst_ne_choose_snd {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : (Set.Nontrivial.choose hs).1 ≠ (Set.Nontrivial.choose hs).2

theorem Set.Nontrivial.mono {α : Type u} {s : Set α} {t : Set α} (hs : Set.Nontrivial s) (hst : s ⊆ t) : Set.Nontrivial t

theorem Set.nontrivial_pair {α : Type u} {x : α} {y : α} (hxy : x ≠ y) : Set.Nontrivial {x, y}

theorem Set.nontrivial_of_pair_subset {α : Type u} {s : Set α} {x : α} {y : α} (hxy : x ≠ y) (h : {x, y} ⊆ s) : Set.Nontrivial s

theorem Set.Nontrivial.pair_subset {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : ∃ (x : α) (y : α), x ≠ y ∧ {x, y} ⊆ s

theorem Set.nontrivial_iff_pair_subset {α : Type u} {s : Set α} : Set.Nontrivial s ↔ ∃ (x : α) (y : α), x ≠ y ∧ {x, y} ⊆ s

theorem Set.nontrivial_of_exists_ne {α : Type u} {s : Set α} {x : α} (hx : x ∈ s) (h : ∃ y ∈ s, y ≠ x) : Set.Nontrivial s

theorem Set.Nontrivial.exists_ne {α : Type u} {s : Set α} (hs : Set.Nontrivial s) (z : α) : ∃ x ∈ s, x ≠ z

theorem Set.nontrivial_iff_exists_ne {α : Type u} {s : Set α} {x : α} (hx : x ∈ s) : Set.Nontrivial s ↔ ∃ y ∈ s, y ≠ x

theorem Set.nontrivial_of_lt {α : Type u} {s : Set α} [Preorder α] {x : α} {y : α} (hx : x ∈ s) (hy : y ∈ s) (hxy : x < y) : Set.Nontrivial s

theorem Set.nontrivial_of_exists_lt {α : Type u} {s : Set α} [Preorder α] (H : ∃ x ∈ s, ∃ y ∈ s, x < y) : Set.Nontrivial s

theorem Set.Nontrivial.exists_lt {α : Type u} {s : Set α} [LinearOrder α] (hs : Set.Nontrivial s) : ∃ x ∈ s, ∃ y ∈ s, x < y

theorem Set.nontrivial_iff_exists_lt {α : Type u} {s : Set α} [LinearOrder α] : Set.Nontrivial s ↔ ∃ x ∈ s, ∃ y ∈ s, x < y

theorem Set.Nontrivial.nonempty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : Set.Nonempty s

theorem Set.Nontrivial.ne_empty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : s ≠ ∅

theorem Set.Nontrivial.not_subset_empty {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : ¬s ⊆ ∅

@[simp]

theorem Set.not_nontrivial_empty {α : Type u} : ¬Set.Nontrivial ∅

@[simp]

theorem Set.not_nontrivial_singleton {α : Type u} {x : α} : ¬Set.Nontrivial {x}

theorem Set.Nontrivial.ne_singleton {α : Type u} {s : Set α} {x : α} (hs : Set.Nontrivial s) : s ≠ {x}

theorem Set.Nontrivial.not_subset_singleton {α : Type u} {s : Set α} {x : α} (hs : Set.Nontrivial s) : ¬s ⊆ {x}

theorem Set.nontrivial_univ {α : Type u} [Nontrivial α] : Set.Nontrivial Set.univ

theorem Set.nontrivial_of_univ_nontrivial {α : Type u} (h : Set.Nontrivial Set.univ) : Nontrivial α

@[simp]

theorem Set.nontrivial_univ_iff {α : Type u} : Set.Nontrivial Set.univ ↔ Nontrivial α

theorem Set.nontrivial_of_nontrivial {α : Type u} {s : Set α} (hs : Set.Nontrivial s) : Nontrivial α

@[simp]

theorem Set.nontrivial_coe_sort {α : Type u} {s : Set α} : Nontrivial ↑s ↔ Set.Nontrivial s

s, coerced to a type, is a nontrivial type if and only if s is a nontrivial set.

theorem Set.Nontrivial.coe_sort {α : Type u} {s : Set α} : Set.Nontrivial s → Nontrivial ↑s

Alias of the reverse direction of Set.nontrivial_coe_sort.

---

s, coerced to a type, is a nontrivial type if and only if s is a nontrivial set.

theorem Set.nontrivial_of_nontrivial_coe {α : Type u} {s : Set α} (hs : Nontrivial ↑s) : Nontrivial α

A type with a set s whose coe_sort is a nontrivial type is nontrivial. For the corresponding result for Subtype, see Subtype.nontrivial_iff_exists_ne.

theorem Set.nontrivial_mono {α : Type u_1} {s : Set α} {t : Set α} (hst : s ⊆ t) (hs : Nontrivial ↑s) : Nontrivial ↑t

@[simp]

theorem Set.not_subsingleton_iff {α : Type u} {s : Set α} : ¬Set.Subsingleton s ↔ Set.Nontrivial s

@[simp]

theorem Set.not_nontrivial_iff {α : Type u} {s : Set α} : ¬Set.Nontrivial s ↔ Set.Subsingleton s

theorem Set.Subsingleton.not_nontrivial {α : Type u} {s : Set α} : Set.Subsingleton s → ¬Set.Nontrivial s

Alias of the reverse direction of Set.not_nontrivial_iff.

theorem Set.Nontrivial.not_subsingleton {α : Type u} {s : Set α} : Set.Nontrivial s → ¬Set.Subsingleton s

Alias of the reverse direction of Set.not_subsingleton_iff.

theorem Set.subsingleton_or_nontrivial {α : Type u} (s : Set α) : Set.Subsingleton s ∨ Set.Nontrivial s

theorem Set.eq_singleton_or_nontrivial {α : Type u} {a : α} {s : Set α} (ha : a ∈ s) : s = {a} ∨ Set.Nontrivial s

theorem Set.nontrivial_iff_ne_singleton {α : Type u} {a : α} {s : Set α} (ha : a ∈ s) : Set.Nontrivial s ↔ s ≠ {a}

theorem Set.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u} {s : Set α} : Set.Nonempty s → (∃ (a : α), s = {a}) ∨ Set.Nontrivial s

theorem Set.univ_eq_true_false : Set.univ = {True, False}

Monotonicity on singletons

theorem Set.Subsingleton.monotoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : MonotoneOn f s

theorem Set.Subsingleton.antitoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : AntitoneOn f s

theorem Set.Subsingleton.strictMonoOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : StrictMonoOn f s

theorem Set.Subsingleton.strictAntiOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : α → β) (h : Set.Subsingleton s) : StrictAntiOn f s

@[simp]

theorem Set.monotoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : MonotoneOn f {a}

@[simp]

theorem Set.antitoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : AntitoneOn f {a}

@[simp]

theorem Set.strictMonoOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : StrictMonoOn f {a}

@[simp]

theorem Set.strictAntiOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : α → β) : StrictAntiOn f {a}