Documentation

Mathlib.Logic.Nontrivial

Nontrivial types #

A type is nontrivial if it contains at least two elements. This is useful in particular for rings (where it is equivalent to the fact that zero is different from one) and for vector spaces (where it is equivalent to the fact that the dimension is positive).

We introduce a typeclass Nontrivial formalizing this property.

class Nontrivial (α : Type u_1) :

In a nontrivial type, there exists a pair of distinct terms.
exists_pair_ne : ∃ x y, x ≠ y

Predicate typeclass for expressing that a type is not reduced to a single element. In rings, this is equivalent to 0 ≠ 1≠ 1. In vector spaces, this is equivalent to positive dimension.

Instances

theorem nontrivial_iff {α : Type u_1} :

Nontrivial α ↔ ∃ x y, x ≠ y

theorem exists_pair_ne (α : Type u_1) [inst : Nontrivial α] :

∃ x y, x ≠ y

theorem Decidable.exists_ne {α : Type u_1} [inst : Nontrivial α] [inst : DecidableEq α] (x : α) :

∃ y, y ≠ x

theorem exists_ne {α : Type u_1} [inst : Nontrivial α] (x : α) :

∃ y, y ≠ x

theorem nontrivial_of_ne {α : Type u_1} (x : α) (y : α) (h : x ≠ y) :

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

theorem exists_pair_lt (α : Type u_1) [inst : Nontrivial α] [inst : LinearOrder α] :

∃ x y, x < y

theorem nontrivial_iff_lt {α : Type u_1} [inst : LinearOrder α] :

Nontrivial α ↔ ∃ x y, x < y

theorem nontrivial_iff_exists_ne {α : Type u_1} (x : α) :

Nontrivial α ↔ ∃ y, y ≠ x

theorem Subtype.nontrivial_iff_exists_ne {α : Type u_1} (p : α → Prop) (x : Subtype p) :

Nontrivial (Subtype p) ↔ ∃ y x, y ≠ ↑x

instance instNontrivialProp :

Nontrivial Prop

Equations

instNontrivialProp = instNontrivialProp.proof_1

instance Nontrivial.to_nonempty {α : Type u_1} [inst : Nontrivial α] :

See Note [lower instance priority]

Note that since this and nonempty_of_inhabited are the most "obvious" way to find a nonempty instance if no direct instance can be found, we give this a higher priority than the usual 100.

Equations

@Nontrivial.to_nonempty = @Nontrivial.to_nonempty.proof_1

noncomputable def nontrivialPSumUnique (α : Type u_1) [inst : 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) }

theorem subsingleton_iff {α : Type u_1} :

Subsingleton α ↔ ∀ (x y : α), x = y

theorem not_nontrivial_iff_subsingleton {α : Type u_1} :

¬Nontrivial α ↔ Subsingleton α

theorem not_nontrivial (α : Type u_1) [inst : Subsingleton α] :

¬Nontrivial α

theorem not_subsingleton (α : Type u_1) [inst : Nontrivial α] :

¬Subsingleton α

theorem subsingleton_or_nontrivial (α : Type u_1) :

Subsingleton α ∨ Nontrivial α

A type is either a subsingleton or nontrivial.

theorem false_of_nontrivial_of_subsingleton (α : Type u_1) [inst : Nontrivial α] [inst : Subsingleton α] :

instance Option.nontrivial {α : Type u_1} [inst : Nonempty α] :

Nontrivial (Option α)

Equations

@Option.nontrivial = @Option.nontrivial.proof_1

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

Pushforward a nontrivial instance along an injective function.

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

Pullback a nontrivial instance along a surjective function.

theorem Function.Injective.exists_ne {α : Type u_1} {β : Type u_2} [inst : 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} [inst : Nonempty α] [inst : Nontrivial β] :

Nontrivial (α × β)

Equations

@nontrivial_prod_right = @nontrivial_prod_right.proof_1

instance nontrivial_prod_left {α : Type u_1} {β : Type u_2} [inst : Nontrivial α] [inst : Nonempty β] :

Nontrivial (α × β)

Equations

@nontrivial_prod_left = @nontrivial_prod_left.proof_1

theorem Pi.nontrivial_at {I : Type u_2} {f : I → Type u_1} (i' : I) [inst : ∀ (i : I), Nonempty (f i)] [inst : 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_1} {f : I → Type u_2} [inst : Inhabited I] [inst : ∀ (i : I), Nonempty (f i)] [inst : 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

@Pi.nontrivial = @Pi.nontrivial.proof_1

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

Nontrivial (α → β)

Equations

@Function.nontrivial = @Function.nontrivial.proof_1

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

x ≤ y

instance Bool.instNontrivialBool :

Nontrivial Bool

Equations

Bool.instNontrivialBool = Bool.instNontrivialBool.proof_1