doc-next-gen

Mathlib.Logic.Nontrivial.Defs

Module docstring

{"# Nontrivial types

A type is nontrivial if it contains at least two elements. This is useful in particular for rings (where it is equivalent to the fact that zero is different from one) and for vector spaces (where it is equivalent to the fact that the dimension is positive).

We introduce a typeclass Nontrivial formalizing this property.

Basic results about nontrivial types are in Mathlib.Logic.Nontrivial.Basic. "}

Nontrivial structure
(α : Type*)
Full source 
/-- Predicate typeclass for expressing that a type is not reduced to a single element. In rings,
this is equivalent to `0 ≠ 1`. In vector spaces, this is equivalent to positive dimension. -/
class Nontrivial (α : Type*) : Prop where
  /-- In a nontrivial type, there exists a pair of distinct terms. -/
  exists_pair_ne : ∃ x y : α, x ≠ y
Nontrivial type
Informal description
A type `α` is called *nontrivial* if it contains at least two distinct elements. This property is particularly useful in ring theory (where it is equivalent to the condition that the additive identity `0` is different from the multiplicative identity `1`) and in vector space theory (where it is equivalent to the space having positive dimension).
exists_pair_ne theorem
(α : Type*) [Nontrivial α] : ∃ x y : α, x ≠ y
Full source 
theorem exists_pair_ne (α : Type*) [Nontrivial α] : ∃ x y : α, x ≠ y :=
  Nontrivial.exists_pair_ne
Existence of Distinct Elements in Nontrivial Types
Informal description
For any nontrivial type $\alpha$, there exist two distinct elements $x$ and $y$ in $\alpha$ such that $x \neq y$.
Decidable.exists_ne theorem
[Nontrivial α] [DecidableEq α] (x : α) : ∃ y, y ≠ x
Full source 
protected theorem Decidable.exists_ne [Nontrivial α] [DecidableEq α] (x : α) : ∃ y, y ≠ x := by
  rcases exists_pair_ne α with ⟨y, y', h⟩
  by_cases hx : x = y
  · rw [← hx] at h
    exact ⟨y', h.symm⟩
  · exact ⟨y, Ne.symm hx⟩
Existence of Distinct Element in Nontrivial Types with Decidable Equality
Informal description
For any nontrivial type $\alpha$ with decidable equality and for any element $x \in \alpha$, there exists an element $y \in \alpha$ such that $y \neq x$.
exists_ne theorem
[Nontrivial α] (x : α) : ∃ y, y ≠ x
Full source 
theorem exists_ne [Nontrivial α] (x : α) : ∃ y, y ≠ x := Decidable.exists_ne x
Existence of Distinct Element in Nontrivial Types
Informal description
For any nontrivial type $\alpha$ and any element $x \in \alpha$, there exists an element $y \in \alpha$ such that $y \neq x$.
nontrivial_of_ne theorem
(x y : α) (h : x ≠ y) : Nontrivial α
Full source 
theorem nontrivial_of_ne (x y : α) (h : x ≠ y) : Nontrivial α :=
  ⟨⟨x, y, h⟩⟩
Nontriviality from Distinct Elements: $x \neq y \implies \text{Nontrivial }\alpha$
Informal description
For any two distinct elements $x$ and $y$ in a type $\alpha$ (i.e., $x \neq y$), the type $\alpha$ is nontrivial.
nontrivial_iff_exists_ne theorem
(x : α) : Nontrivial α ↔ ∃ y, y ≠ x
Full source 
theorem nontrivial_iff_exists_ne (x : α) : NontrivialNontrivial α ↔ ∃ y, y ≠ x :=
  ⟨fun h ↦ @exists_ne α h x, fun ⟨_, hy⟩ ↦ nontrivial_of_ne _ _ hy⟩
Nontriviality Criterion: $\text{Nontrivial }\alpha \leftrightarrow \exists y \neq x$
Informal description
For any element $x$ in a type $\alpha$, the type $\alpha$ is nontrivial if and only if there exists an element $y \in \alpha$ such that $y \neq x$.
instNontrivialProp instance
: Nontrivial Prop
Full source 
instance : Nontrivial Prop :=
  ⟨⟨True, False, true_ne_false⟩⟩
Nontriviality of the Type of Propositions
Informal description
The type of propositions `Prop` is nontrivial, meaning it contains at least two distinct elements (namely `True` and `False`).
Nontrivial.to_nonempty instance
[Nontrivial α] : Nonempty α
Full source 
/-- See Note [lower instance priority]

Note that since this and `instNonemptyOfInhabited` are the most "obvious" way to find a nonempty
instance if no direct instance can be found, we give this a higher priority than the usual `100`.
-/
instance (priority := 500) Nontrivial.to_nonempty [Nontrivial α] : Nonempty α :=
  let ⟨x, _⟩ := _root_.exists_pair_ne α
  ⟨x⟩
Nontrivial Types are Nonempty
Informal description
Every nontrivial type $\alpha$ is nonempty.
not_nontrivial_iff_subsingleton theorem
: ¬Nontrivial α ↔ Subsingleton α
Full source 
theorem not_nontrivial_iff_subsingleton : ¬Nontrivial α¬Nontrivial α ↔ Subsingleton α := by
  simp only [nontrivial_iff, subsingleton_iff, not_exists, Classical.not_not]
Nontriviality and Subsingleton Equivalence: $\neg \text{Nontrivial}\,\alpha \leftrightarrow \text{Subsingleton}\,\alpha$
Informal description
A type $\alpha$ is not nontrivial if and only if it is a subsingleton, i.e., $\neg \text{Nontrivial}\,\alpha \leftrightarrow \text{Subsingleton}\,\alpha$.
not_nontrivial theorem
(α) [Subsingleton α] : ¬Nontrivial α
Full source 
theorem not_nontrivial (α) [Subsingleton α] : ¬Nontrivial α :=
  fun ⟨⟨x, y, h⟩⟩ ↦ h <| Subsingleton.elim x y
Subsingleton Implies Not Nontrivial
Informal description
If a type $\alpha$ is a subsingleton (i.e., has at most one element), then it is not nontrivial.
not_subsingleton theorem
(α) [Nontrivial α] : ¬Subsingleton α
Full source 
theorem not_subsingleton (α) [Nontrivial α] : ¬Subsingleton α :=
  fun _ => not_nontrivial _ ‹_›
Nontrivial Types Are Not Subsingletons
Informal description
If a type $\alpha$ is nontrivial (i.e., contains at least two distinct elements), then it is not a subsingleton (i.e., it cannot have at most one element).
not_subsingleton_iff_nontrivial theorem
: ¬Subsingleton α ↔ Nontrivial α
Full source 
lemma not_subsingleton_iff_nontrivial : ¬ Subsingleton α¬ Subsingleton α ↔ Nontrivial α := by
  rw [← not_nontrivial_iff_subsingleton, Classical.not_not]
Equivalence Between Non-Subsingleton and Nontrivial Types
Informal description
A type $\alpha$ is not a subsingleton (i.e., it has more than one element) if and only if it is nontrivial. In other words, $\neg \text{Subsingleton}\,\alpha \leftrightarrow \text{Nontrivial}\,\alpha$.
subsingleton_or_nontrivial theorem
(α : Type*) : Subsingleton α ∨ Nontrivial α
Full source 
/-- A type is either a subsingleton or nontrivial. -/
theorem subsingleton_or_nontrivial (α : Type*) : SubsingletonSubsingleton α ∨ Nontrivial α := by
  rw [← not_nontrivial_iff_subsingleton, or_comm]
  exact Classical.em _
Subsingleton or Nontrivial Dichotomy
Informal description
For any type $\alpha$, either $\alpha$ is a subsingleton (i.e., all elements are equal) or $\alpha$ is nontrivial (i.e., contains at least two distinct elements).
false_of_nontrivial_of_subsingleton theorem
(α : Type*) [Nontrivial α] [Subsingleton α] : False
Full source 
theorem false_of_nontrivial_of_subsingleton (α : Type*) [Nontrivial α] [Subsingleton α] : False :=
  not_nontrivial _ ‹_›
Contradiction from Nontrivial Subsingleton
Informal description
For any type $\alpha$, if $\alpha$ is both nontrivial and a subsingleton, then this leads to a contradiction (i.e., `False` holds).
Function.Surjective.nontrivial theorem
[Nontrivial β] {f : α → β} (hf : Function.Surjective f) : Nontrivial α
Full source 
/-- Pullback a `Nontrivial` instance along a surjective function. -/
protected theorem Function.Surjective.nontrivial [Nontrivial β] {f : α → β}
    (hf : Function.Surjective f) : Nontrivial α := by
  rcases exists_pair_ne β with ⟨x, y, h⟩
  rcases hf x with ⟨x', hx'⟩
  rcases hf y with ⟨y', hy'⟩
  have : x' ≠ y' := by
    refine fun H ↦ h ?_
    rw [← hx', ← hy', H]
  exact ⟨⟨x', y', this⟩⟩
Nontriviality via Surjective Function
Informal description
If $\beta$ is a nontrivial type and $f : \alpha \to \beta$ is a surjective function, then $\alpha$ is also a nontrivial type.
Bool.instNontrivial instance
: Nontrivial Bool
Full source 
instance : Nontrivial Bool :=
  ⟨⟨true, false, nofun⟩⟩
Nontriviality of the Boolean Type
Informal description
The type of booleans is nontrivial, meaning it contains at least two distinct elements (namely `true` and `false`).