Nontrivial types

Results about Nontrivial.

theorem nontrivial_of_lt {α : Type u_1} [Preorder α] (x : α) (y : α) (h : x < y) : Nontrivial α

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 α] : 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 := { default := default }, uniq := (_ : ∀ (x : α), x = default) }

instance Option.nontrivial {α : Type u_1} [Nonempty α] : Nontrivial (Option α)

Equations

• (_ : Nontrivial (Option α)) = (_ : Nontrivial (Option α))

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

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

• (_ : Nontrivial (α × β)) = (_ : Nontrivial (α × β))

instance nontrivial_prod_left {α : Type u_1} {β : Type u_2} [Nontrivial α] [Nonempty β] : Nontrivial (α × β)

Equations

• (_ : Nontrivial (α × β)) = (_ : Nontrivial (α × β))

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.

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.

Equations

• (_ : Nontrivial ((i : I) → f i)) = (_ : Nontrivial ((i : I) → f i))

instance Function.nontrivial {α : Type u_1} {β : Type u_2} [h : Nonempty α] [Nontrivial β] : Nontrivial (α → β)

Equations

• (_ : Nontrivial (α → β)) = (_ : Nontrivial (α → β))

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