Mathlib.Data.Set.Subsingleton

Set.Subsingleton definition

(s : Set α) : Prop

Full source

/-- A set `s` is a `Subsingleton` if it has at most one element. -/
protected def Subsingleton (s : Set α) : Prop :=
  ∀ ⦃x⦄ (_ : x ∈ s) ⦃y⦄ (_ : y ∈ s), x = y

Subsingleton set

Informal description

A set $s$ is called a *subsingleton* if for any two elements $x, y \in s$, we have $x = y$. In other words, $s$ contains at most one element.

Set.Subsingleton.anti theorem

(ht : t.Subsingleton) (hst : s ⊆ t) : s.Subsingleton

Full source

theorem Subsingleton.anti (ht : t.Subsingleton) (hst : s ⊆ t) : s.Subsingleton := fun _ hx _ hy =>
  ht (hst hx) (hst hy)

Subsingleton Property is Antitone with Respect to Subset Inclusion

Informal description

If a set $t$ is a subsingleton and $s$ is a subset of $t$, then $s$ is also a subsingleton.

Set.subsingleton_empty theorem

: (∅ : Set α).Subsingleton

Full source

@[simp]
theorem subsingleton_empty : (∅ : Set α).Subsingleton := fun _ => False.elim

Empty Set is Subsingleton

Informal description

The empty set $\emptyset$ is a subsingleton set.

Set.subsingleton_singleton theorem

{a} : ({ a } : Set α).Subsingleton

Full source

@[simp]
theorem subsingleton_singleton {a} : ({a} : Set α).Subsingleton := fun _ hx _ hy =>
  (eq_of_mem_singleton hx).symm ▸ (eq_of_mem_singleton hy).symm ▸ rfl

Singleton Sets are Subsingletons

Informal description

For any element $a$ of type $\alpha$, the singleton set $\{a\}$ is a subsingleton, meaning it contains at most one element.

Set.subsingleton_of_subset_singleton theorem

(h : s ⊆ { a }) : s.Subsingleton

Full source

theorem subsingleton_of_subset_singleton (h : s ⊆ {a}) : s.Subsingleton :=
  subsingleton_singleton.anti h

Subsingleton Property of Subsets of Singleton Sets

Informal description

For any set $s$ and element $a$, if $s$ is a subset of the singleton set $\{a\}$, then $s$ is a subsingleton (i.e., $s$ contains at most one element).

Set.subsingleton_of_forall_eq theorem

(a : α) (h : ∀ b ∈ s, b = a) : s.Subsingleton

Full source

theorem subsingleton_of_forall_eq (a : α) (h : ∀ b ∈ s, b = a) : s.Subsingleton := fun _ hb _ hc =>
  (h _ hb).trans (h _ hc).symm

Subsingleton Condition via Universal Equality

Informal description

For any element $a$ of type $\alpha$ and any set $s$ of type $\alpha$, if every element $b \in s$ is equal to $a$, then $s$ is a subsingleton (i.e., $s$ contains at most one element).

Set.subsingleton_iff_singleton theorem

{x} (hx : x ∈ s) : s.Subsingleton ↔ s = { x }

Full source

theorem subsingleton_iff_singleton {x} (hx : x ∈ s) : s.Subsingleton ↔ s = {x} :=
  ⟨fun h => h.eq_singleton_of_mem hx, fun h => h.symm ▸ subsingleton_singleton⟩

Subsingleton iff Singleton for Nonempty Sets

Informal description

For any set $s$ and any element $x \in s$, the set $s$ is a subsingleton (i.e., contains at most one element) if and only if $s$ is equal to the singleton set $\{x\}$.

Set.Subsingleton.induction_on theorem

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

Full source

theorem Subsingleton.induction_on {p : Set α → Prop} (hs : s.Subsingleton) (he : p ∅)
    (h₁ : ∀ x, p {x}) : p s := by
  rcases hs.eq_empty_or_singleton with (rfl | ⟨x, rfl⟩)
  exacts [he, h₁ _]

Induction Principle for Subsingleton Sets

Informal description

Let $s$ be a subsingleton set (i.e., a set with at most one element). For any predicate $p$ on sets, if $p$ holds for the empty set and for every singleton set $\{x\}$, then $p$ holds for $s$.

Set.subsingleton_univ theorem

[Subsingleton α] : (univ : Set α).Subsingleton

Full source

theorem subsingleton_univ [Subsingleton α] : (univ : Set α).Subsingleton := fun x _ y _ =>
  Subsingleton.elim x y

Universal Set is Subsingleton for Subsingleton Type

Informal description

If the type $\alpha$ is a subsingleton (i.e., has at most one element), then the universal set $\text{univ} : \text{Set } \alpha$ is also a subsingleton.

Set.subsingleton_of_univ_subsingleton theorem

(h : (univ : Set α).Subsingleton) : Subsingleton α

Full source

theorem subsingleton_of_univ_subsingleton (h : (univ : Set α).Subsingleton) : Subsingleton α :=
  ⟨fun a b => h (mem_univ a) (mem_univ b)⟩

Subsingleton Type from Subsingleton Universal Set

Informal description

If the universal set `univ : Set α` is a subsingleton (i.e., contains at most one element), then the type `α` itself is a subsingleton (i.e., has at most one element up to equality).

Set.subsingleton_univ_iff theorem

: (univ : Set α).Subsingleton ↔ Subsingleton α

Full source

@[simp]
theorem subsingleton_univ_iff : (univ : Set α).Subsingleton ↔ Subsingleton α :=
  ⟨subsingleton_of_univ_subsingleton, fun h => @subsingleton_univ _ h⟩

Universal Set is Subsingleton iff Type is Subsingleton

Informal description

The universal set $\text{univ} : \text{Set } \alpha$ is a subsingleton if and only if the type $\alpha$ itself is a subsingleton.

Set.Subsingleton.inter_singleton theorem

: (s ∩ { a }).Subsingleton

Full source

lemma Subsingleton.inter_singleton : (s ∩ {a}).Subsingleton :=
  Set.subsingleton_of_subset_singleton Set.inter_subset_right

Intersection with Singleton is Subsingleton

Informal description

For any set $s$ and element $a$, the intersection $s \cap \{a\}$ is a subsingleton (i.e., contains at most one element).

Set.Subsingleton.singleton_inter theorem

: ({ a } ∩ s).Subsingleton

Full source

lemma Subsingleton.singleton_inter : ({a}{a} ∩ s).Subsingleton :=
  Set.subsingleton_of_subset_singleton Set.inter_subset_left

Intersection of Singleton with Any Set is Subsingleton

Informal description

For any set $s$ and element $a$, the intersection $\{a\} \cap s$ is a subsingleton (i.e., contains at most one element).

Set.subsingleton_of_subsingleton theorem

[Subsingleton α] {s : Set α} : Set.Subsingleton s

Full source

theorem subsingleton_of_subsingleton [Subsingleton α] {s : Set α} : Set.Subsingleton s :=
  subsingleton_univ.anti (subset_univ s)

Subsingleton Property of Subsets in a Subsingleton Type

Informal description

For any type $\alpha$ that is a subsingleton (i.e., has at most one element), every subset $s$ of $\alpha$ is also a subsingleton.

Set.subsingleton_isTop theorem

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

Full source

theorem subsingleton_isTop (α : Type*) [PartialOrder α] : Set.Subsingleton { x : α | IsTop x } :=
  fun x hx _ hy => hx.isMax.eq_of_le (hy x)

Uniqueness of Top Elements in a Partial Order

Informal description

For any partially ordered set $\alpha$, the set of top elements $\{x \in \alpha \mid \text{$x$ is a top element}\}$ is a subsingleton (i.e., contains at most one element).

Set.subsingleton_isBot theorem

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

Full source

theorem subsingleton_isBot (α : Type*) [PartialOrder α] : Set.Subsingleton { x : α | IsBot x } :=
  fun x hx _ hy => hx.isMin.eq_of_ge (hy x)

Uniqueness of Bottom Elements in a Partial Order

Informal description

For any partially ordered set $\alpha$, the set of bottom elements $\{x \in \alpha \mid x \text{ is a bottom element}\}$ is a subsingleton (i.e., contains at most one element).

Set.exists_eq_singleton_iff_nonempty_subsingleton theorem

: (∃ a : α, s = { a }) ↔ s.Nonempty ∧ s.Subsingleton

Full source

theorem exists_eq_singleton_iff_nonempty_subsingleton :
    (∃ a : α, s = {a}) ↔ s.Nonempty ∧ s.Subsingleton := by
  refine ⟨?_, fun h => ?_⟩
  · rintro ⟨a, rfl⟩
    exact ⟨singleton_nonempty a, subsingleton_singleton⟩
  · exact h.2.eq_empty_or_singleton.resolve_left h.1.ne_empty

Characterization of Singleton Sets: $s = \{a\} \leftrightarrow s \neq \emptyset \land \text{subsingleton}(s)$

Informal description

A set $s$ is equal to a singleton $\{a\}$ for some element $a$ if and only if $s$ is nonempty and a subsingleton (i.e., contains at most one element).

Set.subsingleton_coe theorem

(s : Set α) : Subsingleton s ↔ s.Subsingleton

Full source

/-- `s`, coerced to a type, is a subsingleton type if and only if `s` is a subsingleton set. -/
@[simp, norm_cast]
theorem subsingleton_coe (s : Set α) : SubsingletonSubsingleton s ↔ s.Subsingleton := by
  constructor
  · refine fun h => fun a ha b hb => ?_
    exact SetCoe.ext_iff.2 (@Subsingleton.elim s h ⟨a, ha⟩ ⟨b, hb⟩)
  · exact fun h => Subsingleton.intro fun a b => SetCoe.ext (h a.property b.property)

Subsingleton Type-Set Equivalence: $\text{Subsingleton}(s) \leftrightarrow \text{Subsingleton}(s)$

Informal description

For any set $s$ of type $\alpha$, the type corresponding to $s$ (obtained by coercing $s$ to a type) is a subsingleton (i.e., has at most one element) if and only if $s$ is a subsingleton set (i.e., contains at most one element).

Set.Subsingleton.coe_sort theorem

{s : Set α} : s.Subsingleton → Subsingleton s

Full source

theorem Subsingleton.coe_sort {s : Set α} : s.Subsingleton → Subsingleton s :=
  s.subsingleton_coe.2

Subsingleton Set Implies Subsingleton Type

Informal description

For any set $s$ of type $\alpha$, if $s$ is a subsingleton (i.e., contains at most one element), then the type corresponding to $s$ (obtained by coercing $s$ to a type) is also a subsingleton (i.e., has at most one element).

Set.subsingleton_coe_of_subsingleton instance

[Subsingleton α] {s : Set α} : Subsingleton s

Full source

/-- The `coe_sort` of a set `s` in a subsingleton type is a subsingleton.
For the corresponding result for `Subtype`, see `subtype.subsingleton`. -/
instance subsingleton_coe_of_subsingleton [Subsingleton α] {s : Set α} : Subsingleton s := by
  rw [s.subsingleton_coe]
  exact subsingleton_of_subsingleton

Subsingleton Type from Subsingleton Set in a Subsingleton Type

Informal description

For any type $\alpha$ that is a subsingleton (i.e., has at most one element) and any subset $s$ of $\alpha$, the type corresponding to $s$ (obtained by coercing $s$ to a type) is also a subsingleton.

Set.Nontrivial definition

(s : Set α) : Prop

Full source

/-- A set `s` is `Set.Nontrivial` if it has at least two distinct elements. -/
protected def Nontrivial (s : Set α) : Prop :=
  ∃ x ∈ s, ∃ y ∈ s, x ≠ y

Nontrivial set

Informal description

A set $s$ is called *nontrivial* if there exist two distinct elements $x$ and $y$ in $s$, i.e., there exist $x \in s$ and $y \in s$ such that $x \neq y$.

Set.nontrivial_of_mem_mem_ne theorem

{x y} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : s.Nontrivial

Full source

theorem nontrivial_of_mem_mem_ne {x y} (hx : x ∈ s) (hy : y ∈ s) (hxy : x ≠ y) : s.Nontrivial :=
  ⟨x, hx, y, hy, hxy⟩

Existence of Distinct Elements Implies Nontriviality of a Set

Informal description

For any set $s$ and elements $x, y \in s$ with $x \neq y$, the set $s$ is nontrivial.

Set.Nontrivial.choose definition

(hs : s.Nontrivial) : α × α

Full source

/-- 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. -/
protected noncomputable def Nontrivial.choose (hs : s.Nontrivial) : α × α :=
  (Exists.choose hs, hs.choose_spec.right.choose)

Selection of distinct elements in a nontrivial set

Informal description

Given a nontrivial set $s$ (i.e., a set containing at least two distinct elements), the function `Set.Nontrivial.choose` selects a pair of distinct elements $(x, y)$ from $s$ such that $x \neq y$.

Set.Nontrivial.choose_fst_mem theorem

(hs : s.Nontrivial) : hs.choose.fst ∈ s

Full source

protected theorem Nontrivial.choose_fst_mem (hs : s.Nontrivial) : hs.choose.fst ∈ s :=
  hs.choose_spec.left

First chosen element of a nontrivial set belongs to the set

Informal description

For any nontrivial set $s$, the first element of the pair selected by `Set.Nontrivial.choose` is an element of $s$.

Set.Nontrivial.choose_snd_mem theorem

(hs : s.Nontrivial) : hs.choose.snd ∈ s

Full source

protected theorem Nontrivial.choose_snd_mem (hs : s.Nontrivial) : hs.choose.snd ∈ s :=
  hs.choose_spec.right.choose_spec.left

Second chosen element of a nontrivial set belongs to the set

Informal description

For any nontrivial set $s$, the second element of the pair selected by `Set.Nontrivial.choose` is an element of $s$.

Set.Nontrivial.choose_fst_ne_choose_snd theorem

(hs : s.Nontrivial) : hs.choose.fst ≠ hs.choose.snd

Full source

protected theorem Nontrivial.choose_fst_ne_choose_snd (hs : s.Nontrivial) :
    hs.choose.fst ≠ hs.choose.snd :=
  hs.choose_spec.right.choose_spec.right

Distinctness of Chosen Elements in a Nontrivial Set

Informal description

For any nontrivial set $s$, the two distinct elements selected by `Set.Nontrivial.choose` satisfy $x \neq y$, where $x$ is the first element and $y$ is the second element of the pair.

Set.Nontrivial.mono theorem

(hs : s.Nontrivial) (hst : s ⊆ t) : t.Nontrivial

Full source

theorem Nontrivial.mono (hs : s.Nontrivial) (hst : s ⊆ t) : t.Nontrivial :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨x, hst hx, y, hst hy, hxy⟩

Monotonicity of Nontriviality under Set Inclusion

Informal description

If a set $s$ is nontrivial and $s$ is a subset of another set $t$, then $t$ is also nontrivial.

Set.nontrivial_pair theorem

{x y} (hxy : x ≠ y) : ({ x, y } : Set α).Nontrivial

Full source

theorem nontrivial_pair {x y} (hxy : x ≠ y) : ({x, y} : Set α).Nontrivial :=
  ⟨x, mem_insert _ _, y, mem_insert_of_mem _ (mem_singleton _), hxy⟩

Pair of distinct elements forms a nontrivial set

Informal description

For any two distinct elements $x$ and $y$ in a type $\alpha$, the set $\{x, y\}$ is nontrivial.

Set.nontrivial_of_pair_subset theorem

{x y} (hxy : x ≠ y) (h : { x, y } ⊆ s) : s.Nontrivial

Full source

theorem nontrivial_of_pair_subset {x y} (hxy : x ≠ y) (h : {x, y}{x, y} ⊆ s) : s.Nontrivial :=
  (nontrivial_pair hxy).mono h

Nontriviality from Pair Inclusion

Informal description

For any two distinct elements $x$ and $y$ in a type $\alpha$, if the set $\{x, y\}$ is a subset of a set $s$, then $s$ is nontrivial.

Set.Nontrivial.pair_subset theorem

(hs : s.Nontrivial) : ∃ x y, x ≠ y ∧ { x, y } ⊆ s

Full source

theorem Nontrivial.pair_subset (hs : s.Nontrivial) : ∃ x y, x ≠ y ∧ {x, y} ⊆ s :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  ⟨x, y, hxy, insert_subset hx <| singleton_subset_iff.2 hy⟩

Existence of a Distinct Pair in a Nontrivial Set

Informal description

If a set $s$ is nontrivial (i.e., contains at least two distinct elements), then there exist two distinct elements $x$ and $y$ in $s$ such that the pair $\{x, y\}$ is a subset of $s$.

Set.nontrivial_iff_pair_subset theorem

: s.Nontrivial ↔ ∃ x y, x ≠ y ∧ { x, y } ⊆ s

Full source

theorem nontrivial_iff_pair_subset : s.Nontrivial ↔ ∃ x y, x ≠ y ∧ {x, y} ⊆ s :=
  ⟨Nontrivial.pair_subset, fun H =>
    let ⟨_, _, hxy, h⟩ := H
    nontrivial_of_pair_subset hxy h⟩

Nontrivial Set Characterization via Distinct Pair Inclusion

Informal description

A set $s$ is nontrivial if and only if there exist two distinct elements $x$ and $y$ in $s$ such that the pair $\{x, y\}$ is a subset of $s$.

Set.nontrivial_of_exists_ne theorem

{x} (hx : x ∈ s) (h : ∃ y ∈ s, y ≠ x) : s.Nontrivial

Full source

theorem nontrivial_of_exists_ne {x} (hx : x ∈ s) (h : ∃ y ∈ s, y ≠ x) : s.Nontrivial :=
  let ⟨y, hy, hyx⟩ := h
  ⟨y, hy, x, hx, hyx⟩

Existence of Distinct Elements Implies Nontriviality of a Set

Informal description

For any element $x$ in a set $s$, if there exists another element $y \in s$ such that $y \neq x$, then $s$ is a nontrivial set.

Set.Nontrivial.exists_ne theorem

(hs : s.Nontrivial) (z) : ∃ x ∈ s, x ≠ z

Full source

theorem Nontrivial.exists_ne (hs : s.Nontrivial) (z) : ∃ x ∈ s, x ≠ z := by
  by_contra! H
  rcases hs with ⟨x, hx, y, hy, hxy⟩
  rw [H x hx, H y hy] at hxy
  exact hxy rfl

Existence of Distinct Element in Nontrivial Set

Informal description

For any nontrivial set $s$ and any element $z$, there exists an element $x \in s$ such that $x \neq z$.

Set.nontrivial_iff_exists_ne theorem

{x} (hx : x ∈ s) : s.Nontrivial ↔ ∃ y ∈ s, y ≠ x

Full source

theorem nontrivial_iff_exists_ne {x} (hx : x ∈ s) : s.Nontrivial ↔ ∃ y ∈ s, y ≠ x :=
  ⟨fun H => H.exists_ne _, nontrivial_of_exists_ne hx⟩

Nontriviality Criterion via Existence of Distinct Element

Informal description

For any element $x$ in a set $s$, the set $s$ is nontrivial if and only if there exists an element $y \in s$ such that $y \neq x$.

Set.nontrivial_of_lt theorem

[Preorder α] {x y} (hx : x ∈ s) (hy : y ∈ s) (hxy : x < y) : s.Nontrivial

Full source

theorem nontrivial_of_lt [Preorder α] {x y} (hx : x ∈ s) (hy : y ∈ s) (hxy : x < y) :
    s.Nontrivial :=
  ⟨x, hx, y, hy, ne_of_lt hxy⟩

Nontriviality from Strict Order in Preordered Sets

Informal description

Let $\alpha$ be a type with a preorder, and let $s$ be a subset of $\alpha$. If there exist elements $x, y \in s$ such that $x < y$, then $s$ is nontrivial (i.e., contains at least two distinct elements).

Set.nontrivial_of_exists_lt theorem

[Preorder α] (H : ∃ᵉ (x ∈ s) (y ∈ s), x < y) : s.Nontrivial

Full source

theorem nontrivial_of_exists_lt [Preorder α]
    (H : ∃ᵉ (x ∈ s) (y ∈ s), x < y) : s.Nontrivial :=
  let ⟨_, hx, _, hy, hxy⟩ := H
  nontrivial_of_lt hx hy hxy

Existence of Strictly Ordered Elements Implies Nontriviality of Set

Informal description

Let $\alpha$ be a type equipped with a preorder, and let $s$ be a subset of $\alpha$. If there exist elements $x, y \in s$ such that $x < y$, then $s$ is nontrivial (i.e., contains at least two distinct elements).

Set.Nontrivial.exists_lt theorem

[LinearOrder α] (hs : s.Nontrivial) : ∃ᵉ (x ∈ s) (y ∈ s), x < y

Full source

theorem Nontrivial.exists_lt [LinearOrder α] (hs : s.Nontrivial) : ∃ᵉ (x ∈ s) (y ∈ s), x < y :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  Or.elim (lt_or_gt_of_ne hxy) (fun H => ⟨x, hx, y, hy, H⟩) fun H => ⟨y, hy, x, hx, H⟩

Existence of Strictly Ordered Elements in Nontrivial Linearly Ordered Sets

Informal description

Let $\alpha$ be a linearly ordered set and $s$ a nontrivial subset of $\alpha$ (i.e., containing at least two distinct elements). Then there exist elements $x, y \in s$ such that $x < y$.

Set.nontrivial_iff_exists_lt theorem

[LinearOrder α] : s.Nontrivial ↔ ∃ᵉ (x ∈ s) (y ∈ s), x < y

Full source

theorem nontrivial_iff_exists_lt [LinearOrder α] :
    s.Nontrivial ↔ ∃ᵉ (x ∈ s) (y ∈ s), x < y :=
  ⟨Nontrivial.exists_lt, nontrivial_of_exists_lt⟩

Nontriviality Criterion for Linearly Ordered Sets: $s$ is Nontrivial $\iff$ $\exists x, y \in s, x < y$

Informal description

For a set $s$ in a linearly ordered type $\alpha$, the set $s$ is nontrivial (contains at least two distinct elements) if and only if there exist elements $x, y \in s$ such that $x < y$.

Set.Nontrivial.nonempty theorem

(hs : s.Nontrivial) : s.Nonempty

Full source

protected theorem Nontrivial.nonempty (hs : s.Nontrivial) : s.Nonempty :=
  let ⟨x, hx, _⟩ := hs
  ⟨x, hx⟩

Nontrivial Sets are Nonempty

Informal description

If a set $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is nonempty.

Set.Nontrivial.ne_empty theorem

(hs : s.Nontrivial) : s ≠ ∅

Full source

protected theorem Nontrivial.ne_empty (hs : s.Nontrivial) : s ≠ ∅ :=
  hs.nonempty.ne_empty

Nontrivial Sets Are Nonempty: $s \neq \emptyset$

Informal description

If a set $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is not equal to the empty set $\emptyset$.

Set.Nontrivial.not_subset_empty theorem

(hs : s.Nontrivial) : ¬s ⊆ ∅

Full source

theorem Nontrivial.not_subset_empty (hs : s.Nontrivial) : ¬s ⊆ ∅ :=
  hs.nonempty.not_subset_empty

Nontrivial Sets Cannot Be Subsets of the Empty Set

Informal description

If a set $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is not a subset of the empty set.

Set.not_nontrivial_empty theorem

: ¬(∅ : Set α).Nontrivial

Full source

@[simp]
theorem not_nontrivial_empty : ¬(∅ : Set α).Nontrivial := fun h => h.ne_empty rfl

Empty Set is Not Nontrivial

Informal description

The empty set $\emptyset$ is not a nontrivial set, i.e., $\neg (\emptyset \text{ is nontrivial})$.

Set.not_nontrivial_singleton theorem

{x} : ¬({ x } : Set α).Nontrivial

Full source

@[simp]
theorem not_nontrivial_singleton {x} : ¬({x} : Set α).Nontrivial := fun H => by
  rw [nontrivial_iff_exists_ne (mem_singleton x)] at H
  let ⟨y, hy, hya⟩ := H
  exact hya (mem_singleton_iff.1 hy)

Singleton Sets Are Not Nontrivial

Informal description

For any element $x$ of type $\alpha$, the singleton set $\{x\}$ is not nontrivial, i.e., it does not contain two distinct elements.

Set.Nontrivial.ne_singleton theorem

{x} (hs : s.Nontrivial) : s ≠ { x }

Full source

theorem Nontrivial.ne_singleton {x} (hs : s.Nontrivial) : s ≠ {x} := fun H => by
  rw [H] at hs
  exact not_nontrivial_singleton hs

Nontrivial Sets Are Not Singletons

Informal description

For any set $s$ and any element $x$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is not equal to the singleton set $\{x\}$.

Set.Nontrivial.not_subset_singleton theorem

{x} (hs : s.Nontrivial) : ¬s ⊆ { x }

Full source

theorem Nontrivial.not_subset_singleton {x} (hs : s.Nontrivial) : ¬s ⊆ {x} :=
  (not_congr subset_singleton_iff_eq).2 (not_or_intro hs.ne_empty hs.ne_singleton)

Nontrivial Sets Cannot Be Subsets of Singletons

Informal description

For any set $s$ and any element $x$, if $s$ is nontrivial (i.e., contains at least two distinct elements), then $s$ is not a subset of the singleton set $\{x\}$.

Set.nontrivial_univ theorem

[Nontrivial α] : (univ : Set α).Nontrivial

Full source

theorem nontrivial_univ [Nontrivial α] : (univ : Set α).Nontrivial :=
  let ⟨x, y, hxy⟩ := exists_pair_ne α
  ⟨x, mem_univ _, y, mem_univ _, hxy⟩

Nontriviality of Universal Set in Nontrivial Types

Informal description

If the type $\alpha$ is nontrivial, then the universal set $\text{univ} = \{x \mid x \in \alpha\}$ is also nontrivial, i.e., there exist two distinct elements in $\text{univ}$.

Set.nontrivial_of_univ_nontrivial theorem

(h : (univ : Set α).Nontrivial) : Nontrivial α

Full source

theorem nontrivial_of_univ_nontrivial (h : (univ : Set α).Nontrivial) : Nontrivial α :=
  let ⟨x, _, y, _, hxy⟩ := h
  ⟨⟨x, y, hxy⟩⟩

Nontriviality of Type from Universal Set

Informal description

If the universal set $\text{univ} = \{x \mid x \in \alpha\}$ is nontrivial (i.e., contains at least two distinct elements), then the type $\alpha$ itself is nontrivial.

Set.nontrivial_univ_iff theorem

: (univ : Set α).Nontrivial ↔ Nontrivial α

Full source

@[simp]
theorem nontrivial_univ_iff : (univ : Set α).Nontrivial ↔ Nontrivial α :=
  ⟨nontrivial_of_univ_nontrivial, fun h => @nontrivial_univ _ h⟩

Nontriviality of Universal Set Equivalence

Informal description

The universal set $\text{univ} = \{x \mid x \in \alpha\}$ is nontrivial (i.e., contains at least two distinct elements) if and only if the type $\alpha$ itself is nontrivial.

Set.singleton_ne_univ theorem

[Nontrivial α] (a : α) : { a } ≠ univ

Full source

@[simp]
theorem singleton_ne_univ [Nontrivial α] (a : α) : {a}{a} ≠ univ :=
  nonempty_compl.mp (nonempty_compl_of_nontrivial a)

Singleton Set is Not Universal in Nontrivial Types

Informal description

If a type $\alpha$ is nontrivial (i.e., contains at least two distinct elements), then for any element $a \in \alpha$, the singleton set $\{a\}$ is not equal to the universal set $\text{univ}$ (the set of all elements of $\alpha$).

Set.singleton_ssubset_univ theorem

[Nontrivial α] (a : α) : { a } ⊂ univ

Full source

@[simp]
theorem singleton_ssubset_univ [Nontrivial α] (a : α) : {a}{a} ⊂ univ :=
  ssubset_univ_iff.mpr <| singleton_ne_univ a

Singleton is Strict Subset of Universal Set in Nontrivial Types

Informal description

For any nontrivial type $\alpha$ (i.e., a type with at least two distinct elements) and any element $a \in \alpha$, the singleton set $\{a\}$ is a strict subset of the universal set $\text{univ}$ (the set of all elements of $\alpha$).

Set.nontrivial_of_nontrivial theorem

(hs : s.Nontrivial) : Nontrivial α

Full source

theorem nontrivial_of_nontrivial (hs : s.Nontrivial) : Nontrivial α :=
  let ⟨x, _, y, _, hxy⟩ := hs
  ⟨⟨x, y, hxy⟩⟩

Nontriviality of Type from Nontrivial Set

Informal description

If a set $s$ is nontrivial (i.e., contains at least two distinct elements), then the ambient type $\alpha$ is also nontrivial.

Set.nontrivial_coe_sort theorem

{s : Set α} : Nontrivial s ↔ s.Nontrivial

Full source

/-- `s`, coerced to a type, is a nontrivial type if and only if `s` is a nontrivial set. -/
@[simp, norm_cast]
theorem nontrivial_coe_sort {s : Set α} : NontrivialNontrivial s ↔ s.Nontrivial := by
  simp [← nontrivial_univ_iff, Set.Nontrivial]

Equivalence of Nontriviality for Set Coercion

Informal description

For any set $s$ of type $\alpha$, the type obtained by coercing $s$ to a type is nontrivial (i.e., contains at least two distinct elements) if and only if $s$ is a nontrivial set (i.e., contains at least two distinct elements).

Set.nontrivial_of_nontrivial_coe theorem

(hs : Nontrivial s) : Nontrivial α

Full source

/-- 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 nontrivial_of_nontrivial_coe (hs : Nontrivial s) : Nontrivial α :=
  nontrivial_of_nontrivial <| nontrivial_coe_sort.1 hs

Nontriviality of Ambient Type from Nontrivial Coerced Set

Informal description

If the type obtained by coercing a set $s$ to a type is nontrivial (i.e., contains at least two distinct elements), then the ambient type $\alpha$ is also nontrivial.

Set.nontrivial_mono theorem

{α : Type*} {s t : Set α} (hst : s ⊆ t) (hs : Nontrivial s) : Nontrivial t

Full source

theorem nontrivial_mono {α : Type*} {s t : Set α} (hst : s ⊆ t) (hs : Nontrivial s) :
    Nontrivial t :=
  Nontrivial.coe_sort <| (nontrivial_coe_sort.1 hs).mono hst

Monotonicity of Nontriviality under Set Inclusion

Informal description

For any type $\alpha$ and sets $s, t \subseteq \alpha$, if $s$ is a nontrivial subset of $t$ (i.e., $s$ contains at least two distinct elements and $s \subseteq t$), then $t$ is also nontrivial.

Set.not_subsingleton_iff theorem

: ¬s.Subsingleton ↔ s.Nontrivial

Full source

@[simp]
theorem not_subsingleton_iff : ¬s.Subsingleton¬s.Subsingleton ↔ s.Nontrivial := by
  simp_rw [Set.Subsingleton, Set.Nontrivial, not_forall, exists_prop]

Characterization of Nontrivial Sets via Non-Subsingletons

Informal description

A set $s$ is not a subsingleton if and only if it is nontrivial, i.e., $\neg \text{Subsingleton}(s) \leftrightarrow \text{Nontrivial}(s)$.

Set.not_nontrivial_iff theorem

: ¬s.Nontrivial ↔ s.Subsingleton

Full source

@[simp]
theorem not_nontrivial_iff : ¬s.Nontrivial¬s.Nontrivial ↔ s.Subsingleton :=
  Iff.not_left not_subsingleton_iff.symm

Characterization of Subsingleton Sets via Non-Nontriviality

Informal description

A set $s$ is not nontrivial if and only if it is a subsingleton, i.e., $\neg \text{Nontrivial}(s) \leftrightarrow \text{Subsingleton}(s)$.

Set.subsingleton_or_nontrivial theorem

(s : Set α) : s.Subsingleton ∨ s.Nontrivial

Full source

protected lemma subsingleton_or_nontrivial (s : Set α) : s.Subsingleton ∨ s.Nontrivial := by
  simp [or_iff_not_imp_right]

Subsingleton or Nontrivial Dichotomy for Sets

Informal description

For any set $s$ in a type $\alpha$, either $s$ is a subsingleton (contains at most one element) or $s$ is nontrivial (contains at least two distinct elements).

Set.nontrivial_iff_ne_singleton theorem

(ha : a ∈ s) : s.Nontrivial ↔ s ≠ { a }

Full source

lemma nontrivial_iff_ne_singleton (ha : a ∈ s) : s.Nontrivial ↔ s ≠ {a} :=
  ⟨Nontrivial.ne_singleton, (eq_singleton_or_nontrivial ha).resolve_left⟩

Nontrivial Set Characterization via Non-Singleton Condition

Informal description

For any set $s$ and any element $a \in s$, the set $s$ is nontrivial (i.e., contains at least two distinct elements) if and only if $s$ is not equal to the singleton set $\{a\}$.

Set.Nonempty.exists_eq_singleton_or_nontrivial theorem

: s.Nonempty → (∃ a, s = { a }) ∨ s.Nontrivial

Full source

lemma Nonempty.exists_eq_singleton_or_nontrivial : s.Nonempty → (∃ a, s = {a}) ∨ s.Nontrivial :=
  fun ⟨a, ha⟩ ↦ (eq_singleton_or_nontrivial ha).imp_left <| Exists.intro a

Characterization of Nonempty Sets as Singletons or Nontrivial Sets

Informal description

For any nonempty set $s$, either there exists an element $a$ such that $s$ is the singleton set $\{a\}$, or $s$ is nontrivial (i.e., contains at least two distinct elements).

Set.univ_eq_true_false theorem

: univ = ({ True, False } : Set Prop)

Full source

theorem univ_eq_true_false : univ = ({True, False} : Set Prop) :=
  Eq.symm <| eq_univ_of_forall fun x => by
    rw [mem_insert_iff, mem_singleton_iff]
    exact Classical.propComplete x

Universal Set of Propositions Equals {True, False}

Informal description

The universal set of propositions is equal to the set containing exactly the propositions `True` and `False`, i.e., $\text{univ} = \{\text{True}, \text{False}\}$ where $\text{univ}$ denotes the universal set of all propositions.

Set.Subsingleton.monotoneOn theorem

(h : s.Subsingleton) : MonotoneOn f s

Full source

protected theorem Subsingleton.monotoneOn (h : s.Subsingleton) : MonotoneOn f s :=
  fun _ ha _ hb _ => (congr_arg _ (h ha hb)).le

Monotonicity on Subsingleton Sets

Informal description

If a set $s$ is a subsingleton (i.e., contains at most one element), then any function $f$ is monotone on $s$.

Set.Subsingleton.antitoneOn theorem

(h : s.Subsingleton) : AntitoneOn f s

Full source

protected theorem Subsingleton.antitoneOn (h : s.Subsingleton) : AntitoneOn f s :=
  fun _ ha _ hb _ => (congr_arg _ (h hb ha)).le

Antitonicity on Subsingleton Sets

Informal description

If a set $s$ is a subsingleton (i.e., contains at most one element), then any function $f$ is antitone on $s$.

Set.Subsingleton.strictMonoOn theorem

(h : s.Subsingleton) : StrictMonoOn f s

Full source

protected theorem Subsingleton.strictMonoOn (h : s.Subsingleton) : StrictMonoOn f s :=
  fun _ ha _ hb hlt => (hlt.ne (h ha hb)).elim

Strict Monotonicity on Subsingleton Sets

Informal description

If a set $s$ is a subsingleton (i.e., contains at most one element), then any function $f$ is strictly monotone on $s$.

Set.Subsingleton.strictAntiOn theorem

(h : s.Subsingleton) : StrictAntiOn f s

Full source

protected theorem Subsingleton.strictAntiOn (h : s.Subsingleton) : StrictAntiOn f s :=
  fun _ ha _ hb hlt => (hlt.ne (h ha hb)).elim

Strictly Antitone Functions on Subsingleton Sets

Informal description

For any function $f$ and any subsingleton set $s$, the function $f$ is strictly antitone on $s$.

Set.monotoneOn_singleton theorem

: MonotoneOn f { a }

Full source

@[simp]
theorem monotoneOn_singleton : MonotoneOn f {a} :=
  subsingleton_singleton.monotoneOn f

Monotonicity on Singleton Sets

Informal description

For any function $f$ and any singleton set $\{a\}$, the function $f$ is monotone on $\{a\}$.

Set.antitoneOn_singleton theorem

: AntitoneOn f { a }

Full source

@[simp]
theorem antitoneOn_singleton : AntitoneOn f {a} :=
  subsingleton_singleton.antitoneOn f

Antitonicity on Singleton Sets

Informal description

For any function $f$ and any singleton set $\{a\}$, the function $f$ is antitone on $\{a\}$.

Set.strictMonoOn_singleton theorem

: StrictMonoOn f { a }

Full source

@[simp]
theorem strictMonoOn_singleton : StrictMonoOn f {a} :=
  subsingleton_singleton.strictMonoOn f

Strict Monotonicity on Singleton Sets

Informal description

For any function $f$ and any singleton set $\{a\}$, the function $f$ is strictly monotone on $\{a\}$.

Set.strictAntiOn_singleton theorem

: StrictAntiOn f { a }

Full source

@[simp]
theorem strictAntiOn_singleton : StrictAntiOn f {a} :=
  subsingleton_singleton.strictAntiOn f

Strictly Antitone Functions on Singleton Sets

Informal description

For any function $f$ and any singleton set $\{a\}$, the function $f$ is strictly antitone on $\{a\}$.