Documentation

Mathlib.Logic.Nontrivial.Defs

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.

source
class Nontrivial (α : Type u_3) :
Prop

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.

  • exists_pair_ne : ∃ (x : α), ∃ (y : α), x ≠ y

    In a nontrivial type, there exists a pair of distinct terms.

Instances
    source
    theorem nontrivial_iff {α : Type u_1} :
    Nontrivial α ↔ ∃ (x : α), ∃ (y : α), x ≠ y
    source
    theorem exists_pair_ne (α : Type u_3) [Nontrivial α] :
    ∃ (x : α), ∃ (y : α), x ≠ y
    source
    theorem Decidable.exists_ne {α : Type u_1} [Nontrivial α] [DecidableEq α] (x : α) :
    ∃ (y : α), y ≠ x
    source
    theorem exists_ne {α : Type u_1} [Nontrivial α] (x : α) :
    ∃ (y : α), y ≠ x
    source
    theorem nontrivial_of_ne {α : Type u_1} (x : α) (y : α) (h : x ≠ y) :
    Nontrivial α
    source
    theorem nontrivial_iff_exists_ne {α : Type u_1} (x : α) :
    Nontrivial α ↔ ∃ (y : α), y ≠ x
    source
    instance instNontrivialProp :
    Nontrivial Prop
    Equations
    source
    instance Nontrivial.to_nonempty {α : Type u_1} [Nontrivial α] :
    Nonempty α

    See Note [lower instance priority]

    Note that since this and nonempty_of_inhabited 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.

    Equations
    source
    theorem subsingleton_iff {α : Type u_1} :
    Subsingleton α ↔ ∀ (x y : α), x = y
    source
    theorem not_nontrivial_iff_subsingleton {α : Type u_1} :
    ¬Nontrivial α ↔ Subsingleton α
    source
    theorem not_nontrivial (α : Type u_3) [Subsingleton α] :
    ¬Nontrivial α
    source
    theorem not_subsingleton (α : Type u_3) [Nontrivial α] :
    ¬Subsingleton α
    source
    theorem not_subsingleton_iff_nontrivial {α : Type u_1} :
    ¬Subsingleton α ↔ Nontrivial α
    source
    theorem subsingleton_or_nontrivial (α : Type u_3) :
    Subsingleton α ∨ Nontrivial α

    A type is either a subsingleton or nontrivial.

    source
    theorem false_of_nontrivial_of_subsingleton (α : Type u_3) [Nontrivial α] [Subsingleton α] :
    False
    source
    theorem Function.Surjective.nontrivial {α : Type u_1} {β : Type u_2} [Nontrivial β] {f : α → β} (hf : Function.Surjective f) :
    Nontrivial α

    Pullback a Nontrivial instance along a surjective function.

    source
    instance Bool.instNontrivialBool :
    Nontrivial Bool
    Equations