Documentation

Mathlib.Logic.Nontrivial.Basic

Nontrivial types #

Results about Nontrivial.

theorem nontrivial_of_lt {α : Type u_1} [Preorder α] (x : α) (y : α) (h : x < y) :
theorem exists_pair_lt (α : Type u_3) [Nontrivial α] [LinearOrder α] :
∃ (x : α), ∃ (y : α), x < y
theorem nontrivial_iff_lt {α : Type u_1} [LinearOrder α] :
Nontrivial α ∃ (x : α), ∃ (y : α), x < y
theorem Subtype.nontrivial_iff_exists_ne {α : Type u_1} (p : αProp) (x : Subtype p) :
Nontrivial (Subtype p) ∃ (y : α), ∃ (x_1 : p y), y x
noncomputable def nontrivialPSumUnique (α : Type u_3) [Inhabited α] :

An inhabited type is either nontrivial, or has a unique element.

Equations
Instances For
    instance Option.nontrivial {α : Type u_1} [Nonempty α] :
    Equations
    theorem Function.Injective.nontrivial {α : Type u_1} {β : Type u_2} [Nontrivial α] {f : αβ} (hf : Function.Injective f) :

    Pushforward a Nontrivial instance along an injective function.

    theorem Function.Injective.exists_ne {α : Type u_1} {β : Type u_2} [Nontrivial α] {f : αβ} (hf : Function.Injective f) (y : β) :
    ∃ (x : α), f x y

    An injective function from a nontrivial type has an argument at which it does not take a given value.

    instance nontrivial_prod_right {α : Type u_1} {β : Type u_2} [Nonempty α] [Nontrivial β] :
    Nontrivial (α × β)
    Equations
    instance nontrivial_prod_left {α : Type u_1} {β : Type u_2} [Nontrivial α] [Nonempty β] :
    Nontrivial (α × β)
    Equations
    theorem Pi.nontrivial_at {I : Type u_3} {f : IType u_4} (i' : I) [inst : ∀ (i : I), Nonempty (f i)] [Nontrivial (f i')] :
    Nontrivial ((i : I) → f i)

    A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere.

    instance Pi.nontrivial {I : Type u_3} {f : IType u_4} [Inhabited I] [∀ (i : I), Nonempty (f i)] [Nontrivial (f default)] :
    Nontrivial ((i : I) → f i)

    As a convenience, provide an instance automatically if (f default) is nontrivial.

    If a different index has the non-trivial type, then use haveI := nontrivial_at that_index.

    Equations
    instance Function.nontrivial {α : Type u_1} {β : Type u_2} [h : Nonempty α] [Nontrivial β] :
    Nontrivial (αβ)
    Equations
    theorem Subsingleton.le {α : Type u_1} [Preorder α] [Subsingleton α] (x : α) (y : α) :
    x y
    theorem Subsingleton.eq_zero {α : Type u_1} [Zero α] [Subsingleton α] (a : α) :
    a = 0
    theorem Subsingleton.eq_one {α : Type u_1} [One α] [Subsingleton α] (a : α) :
    a = 1