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.val

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 := ⋯ }

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

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

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

instance instNontrivialSum {α : Type u_1} {β : Type u_2} [Nontrivial α] : Nontrivial (α ⊕ β)

instance instNontrivialSum_1 {α : Type u_1} {β : Type u_2} [Nontrivial β] : Nontrivial (α ⊕ β)

instance instNontrivialSumOfNonempty {α : Type u_1} {β : Type u_2} [Nonempty α] [Nonempty β] : Nontrivial (α ⊕ β)

instance instSubsingletonSumOfIsEmpty {α : Type u_1} {β : Type u_2} [Subsingleton α] [IsEmpty β] : Subsingleton (α ⊕ β)

instance instSubsingletonSumOfIsEmpty_1 {α : Type u_1} {β : Type u_2} [IsEmpty α] [Subsingleton β] : Subsingleton (α ⊕ β)

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.

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

theorem Subsingleton.le {α : Type u_1} [Preorder α] [Subsingleton α] (x y : α) : x ≤ y