Documentation

Mathlib.Data.Set.Subsingleton

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 α) :

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

Equations
  • s.Subsingleton = ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sx = y
Instances For
    theorem Set.Subsingleton.anti {α : Type u} {s : Set α} {t : Set α} (ht : t.Subsingleton) (hst : s t) :
    s.Subsingleton
    theorem Set.Subsingleton.eq_singleton_of_mem {α : Type u} {s : Set α} (hs : s.Subsingleton) {x : α} (hx : x s) :
    s = {x}
    @[simp]
    theorem Set.subsingleton_empty {α : Type u} :
    .Subsingleton
    @[simp]
    theorem Set.subsingleton_singleton {α : Type u} {a : α} :
    {a}.Subsingleton
    theorem Set.subsingleton_of_subset_singleton {α : Type u} {a : α} {s : Set α} (h : s {a}) :
    s.Subsingleton
    theorem Set.subsingleton_of_forall_eq {α : Type u} {s : Set α} (a : α) (h : bs, b = a) :
    s.Subsingleton
    theorem Set.subsingleton_iff_singleton {α : Type u} {s : Set α} {x : α} (hx : x s) :
    s.Subsingleton s = {x}
    theorem Set.Subsingleton.eq_empty_or_singleton {α : Type u} {s : Set α} (hs : s.Subsingleton) :
    s = ∃ (x : α), s = {x}
    theorem Set.Subsingleton.induction_on {α : Type u} {s : Set α} {p : Set αProp} (hs : s.Subsingleton) (he : p ) (h₁ : ∀ (x : α), p {x}) :
    p s
    theorem Set.subsingleton_univ {α : Type u} [Subsingleton α] :
    Set.univ.Subsingleton
    theorem Set.subsingleton_of_univ_subsingleton {α : Type u} (h : Set.univ.Subsingleton) :
    @[simp]
    theorem Set.subsingleton_univ_iff {α : Type u} :
    Set.univ.Subsingleton Subsingleton α
    theorem Set.Subsingleton.inter_singleton {α : Type u} {a : α} {s : Set α} :
    (s {a}).Subsingleton
    theorem Set.Subsingleton.singleton_inter {α : Type u} {a : α} {s : Set α} :
    ({a} s).Subsingleton
    theorem Set.subsingleton_of_subsingleton {α : Type u} [Subsingleton α] {s : Set α} :
    s.Subsingleton
    theorem Set.subsingleton_isTop (α : Type u_1) [PartialOrder α] :
    {x : α | IsTop x}.Subsingleton
    theorem Set.subsingleton_isBot (α : Type u_1) [PartialOrder α] :
    {x : α | IsBot x}.Subsingleton
    theorem Set.exists_eq_singleton_iff_nonempty_subsingleton {α : Type u} {s : Set α} :
    (∃ (a : α), s = {a}) s.Nonempty s.Subsingleton
    @[simp]
    theorem Set.subsingleton_coe {α : Type u} (s : Set α) :
    Subsingleton s s.Subsingleton

    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 α} :
    s.SubsingletonSubsingleton 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 α) :

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

    Equations
    • s.Nontrivial = xs, ys, x y
    Instances For
      theorem Set.nontrivial_of_mem_mem_ne {α : Type u} {s : Set α} {x : α} {y : α} (hx : x s) (hy : y s) (hxy : x y) :
      s.Nontrivial
      noncomputable def Set.Nontrivial.choose {α : Type u} {s : Set α} (hs : s.Nontrivial) :
      α × α

      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
      Instances For
        theorem Set.Nontrivial.choose_fst_mem {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        hs.choose.1 s
        theorem Set.Nontrivial.choose_snd_mem {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        hs.choose.2 s
        theorem Set.Nontrivial.choose_fst_ne_choose_snd {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        hs.choose.1 hs.choose.2
        theorem Set.Nontrivial.mono {α : Type u} {s : Set α} {t : Set α} (hs : s.Nontrivial) (hst : s t) :
        t.Nontrivial
        theorem Set.nontrivial_pair {α : Type u} {x : α} {y : α} (hxy : x y) :
        {x, y}.Nontrivial
        theorem Set.nontrivial_of_pair_subset {α : Type u} {s : Set α} {x : α} {y : α} (hxy : x y) (h : {x, y} s) :
        s.Nontrivial
        theorem Set.Nontrivial.pair_subset {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        ∃ (x : α) (y : α), x y {x, y} s
        theorem Set.nontrivial_iff_pair_subset {α : Type u} {s : Set α} :
        s.Nontrivial ∃ (x : α) (y : α), x y {x, y} s
        theorem Set.nontrivial_of_exists_ne {α : Type u} {s : Set α} {x : α} (hx : x s) (h : ys, y x) :
        s.Nontrivial
        theorem Set.Nontrivial.exists_ne {α : Type u} {s : Set α} (hs : s.Nontrivial) (z : α) :
        xs, x z
        theorem Set.nontrivial_iff_exists_ne {α : Type u} {s : Set α} {x : α} (hx : x s) :
        s.Nontrivial ys, y x
        theorem Set.nontrivial_of_lt {α : Type u} {s : Set α} [Preorder α] {x : α} {y : α} (hx : x s) (hy : y s) (hxy : x < y) :
        s.Nontrivial
        theorem Set.nontrivial_of_exists_lt {α : Type u} {s : Set α} [Preorder α] (H : xs, ys, x < y) :
        s.Nontrivial
        theorem Set.Nontrivial.exists_lt {α : Type u} {s : Set α} [LinearOrder α] (hs : s.Nontrivial) :
        xs, ys, x < y
        theorem Set.nontrivial_iff_exists_lt {α : Type u} {s : Set α} [LinearOrder α] :
        s.Nontrivial xs, ys, x < y
        theorem Set.Nontrivial.nonempty {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        s.Nonempty
        theorem Set.Nontrivial.ne_empty {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        theorem Set.Nontrivial.not_subset_empty {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        @[simp]
        theorem Set.not_nontrivial_empty {α : Type u} :
        ¬.Nontrivial
        @[simp]
        theorem Set.not_nontrivial_singleton {α : Type u} {x : α} :
        ¬{x}.Nontrivial
        theorem Set.Nontrivial.ne_singleton {α : Type u} {s : Set α} {x : α} (hs : s.Nontrivial) :
        s {x}
        theorem Set.Nontrivial.not_subset_singleton {α : Type u} {s : Set α} {x : α} (hs : s.Nontrivial) :
        ¬s {x}
        theorem Set.nontrivial_univ {α : Type u} [Nontrivial α] :
        Set.univ.Nontrivial
        theorem Set.nontrivial_of_univ_nontrivial {α : Type u} (h : Set.univ.Nontrivial) :
        @[simp]
        theorem Set.nontrivial_univ_iff {α : Type u} :
        Set.univ.Nontrivial Nontrivial α
        theorem Set.nontrivial_of_nontrivial {α : Type u} {s : Set α} (hs : s.Nontrivial) :
        @[simp]
        theorem Set.nontrivial_coe_sort {α : Type u} {s : Set α} :
        Nontrivial s s.Nontrivial

        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 α} :
        s.NontrivialNontrivial 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) :

        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) :
        @[simp]
        theorem Set.not_subsingleton_iff {α : Type u} {s : Set α} :
        ¬s.Subsingleton s.Nontrivial
        @[simp]
        theorem Set.not_nontrivial_iff {α : Type u} {s : Set α} :
        ¬s.Nontrivial s.Subsingleton
        theorem Set.Subsingleton.not_nontrivial {α : Type u} {s : Set α} :
        s.Subsingleton¬s.Nontrivial

        Alias of the reverse direction of Set.not_nontrivial_iff.

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

        Alias of the reverse direction of Set.not_subsingleton_iff.

        theorem Set.subsingleton_or_nontrivial {α : Type u} (s : Set α) :
        s.Subsingleton s.Nontrivial
        theorem Set.eq_singleton_or_nontrivial {α : Type u} {a : α} {s : Set α} (ha : a s) :
        s = {a} s.Nontrivial
        theorem Set.nontrivial_iff_ne_singleton {α : Type u} {a : α} {s : Set α} (ha : a s) :
        s.Nontrivial s {a}
        theorem Set.Nonempty.exists_eq_singleton_or_nontrivial {α : Type u} {s : Set α} :
        s.Nonempty(∃ (a : α), s = {a}) s.Nontrivial

        Monotonicity on singletons #

        theorem Set.Subsingleton.monotoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : s.Subsingleton) :
        theorem Set.Subsingleton.antitoneOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : s.Subsingleton) :
        theorem Set.Subsingleton.strictMonoOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : s.Subsingleton) :
        theorem Set.Subsingleton.strictAntiOn {α : Type u} {β : Type v} {s : Set α} [Preorder α] [Preorder β] (f : αβ) (h : s.Subsingleton) :
        @[simp]
        theorem Set.monotoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :
        @[simp]
        theorem Set.antitoneOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :
        @[simp]
        theorem Set.strictMonoOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :
        @[simp]
        theorem Set.strictAntiOn_singleton {α : Type u} {β : Type v} {a : α} [Preorder α] [Preorder β] (f : αβ) :