# Nontrivial types #

Results about `Nontrivial`.

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

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

Equations

- nontrivialPSumUnique α = if h : Nontrivial α then PSum.inl h else PSum.inr { toInhabited := inst✝, uniq := ⋯ }

Instances For

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

Pushforward a `Nontrivial` instance along an injective function.

source
theorem Function.Injective.exists_ne {α : Type u_1} {β : Type u_2} [Nontrivial α] {f : α → β} (hf : 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.

source
instance nontrivial_prod_right {α : Type u_1} {β : Type u_2} [Nonempty α] [Nontrivial β] :
Nontrivial (α × β)
source
instance nontrivial_prod_left {α : Type u_1} {β : Type u_2} [Nontrivial α] [Nonempty β] :
Nontrivial (α × β)
source
theorem Pi.nontrivial_at {I : Type u_3} {f : I → Type 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.

source
instance Pi.nontrivial {I : Type u_3} {f : I → Type 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`.

source
instance Function.nontrivial {α : Type u_1} {β : Type u_2} [h : Nonempty α] [Nontrivial β] :
Nontrivial (α → β)
source
theorem Subsingleton.le {α : Type u_1} [Preorder α] [Subsingleton α] (x y : α) :
x ≤ y