# Nontrivial types #

Results about Nontrivial.

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

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

Equations
• = if h : then else PSum.inr { default := default, uniq := }
Instances For
instance Option.nontrivial {α : Type u_1} [] :
Equations
• =
theorem Function.Injective.nontrivial {α : Type u_1} {β : Type u_2} [] {f : αβ} (hf : ) :

Pushforward a Nontrivial instance along an injective function.

theorem Function.Injective.exists_ne {α : Type u_1} {β : Type u_2} [] {f : αβ} (hf : ) (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} [] [] :
Nontrivial (α × β)
Equations
• =
instance nontrivial_prod_left {α : Type u_1} {β : Type u_2} [] [] :
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} [] [∀ (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 : ] [] :
Nontrivial (αβ)
Equations
• =
theorem Subsingleton.le {α : Type u_1} [] [] (x : α) (y : α) :
x y
theorem Subsingleton.eq_zero {α : Type u_1} [Zero α] [] (a : α) :
a = 0
theorem Subsingleton.eq_one {α : Type u_1} [One α] [] (a : α) :
a = 1