mathlib documentation

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.

theorem nontrivial_iff {α : Type u_1} :
nontrivial α ∃ (x y : α), x y

theorem exists_pair_ne (α : Type u_1) [nontrivial α] :
∃ (x y : α), x y

theorem exists_ne {α : Type u_1} [nontrivial α] (x : α) :
∃ (y : α), y x

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

theorem nontrivial_of_lt {α : Type u_1} [preorder α] (x y : α) :
x < ynontrivial α

@[instance]
def nontrivial.to_nonempty {α : Type u_1} [nontrivial α] :

def nontrivial_psum_unique (α : Type u_1) [inhabited α] :

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

Equations
theorem subsingleton_iff {α : Type u_1} :
subsingleton α ∀ (x y : α), x = y

theorem not_subsingleton (α : Type u_1) [h : nontrivial α] :

theorem subsingleton_or_nontrivial (α : Type u_1) :

A type is either a subsingleton or nontrivial.

@[instance]
def nontrivial_prod_left {α : Type u_1} {β : Type u_2} [nontrivial α] [nonempty β] :
nontrivial × β)

@[instance]
def nontrivial_prod_right {α : Type u_1} {β : Type u_2} [nontrivial α] [nonempty β] :
nontrivial × α)

@[instance]
def option.nontrivial {α : Type u_1} [nonempty α] :

@[instance]
def function.nontrivial {α : Type u_1} {β : Type u_2} [nonempty α] [nontrivial β] :
nontrivial (α → β)

theorem function.injective.nontrivial {α : Type u_1} {β : Type u_2} [nontrivial α] {f : α → β} :

Pushforward a nontrivial instance along an injective function.

theorem function.surjective.nontrivial {α : Type u_1} {β : Type u_2} [nontrivial β] {f : α → β} :

Pullback a nontrivial instance along a surjective 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.

Simp lemmas for nontriviality tactic

theorem subsingleton.le {α : Type u_1} [preorder α] [subsingleton α] (x y : α) :
x y

Tries to generate a nontrivial α instance by performing case analysis on subsingleton_or_nontrivial α, attempting to discharge the subsingleton branch using lemmas with @[nontriviality] attribute, including subsingleton.le and eq_iff_true_of_subsingleton.

Tries to generate a nontrivial α instance using nontrivial_of_ne or nontrivial_of_lt and local hypotheses.

Attempts to generate a nontrivial α hypothesis.

The tactic first looks for an instance using apply_instance.

If the goal is an (in)equality, the type α is inferred from the goal. Otherwise, the type needs to be specified in the tactic invocation, as nontriviality α.

The nontriviality tactic will first look for strict inequalities amongst the hypotheses, and use these to derive the nontrivial instance directly.

Otherwise, it will perform a case split on subsingleton α ∨ nontrivial α, and attempt to discharge the subsingleton goal using simp [lemmas] with nontriviality, where [lemmas] is a list of additional simp lemmas that can be passed to nontriviality using the syntax nontriviality α using [lemmas].

example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : 0 < a :=
begin
  nontriviality, -- There is now a `nontrivial R` hypothesis available.
  assumption,
end
example {R : Type} [comm_ring R] {r s : R} : r * s = s * r :=
begin
  nontriviality, -- There is now a `nontrivial R` hypothesis available.
  apply mul_comm,
end
example {R : Type} [ordered_ring R] {a : R} (h : 0 < a) : (2 : )  4 :=
begin
  nontriviality R, -- there is now a `nontrivial R` hypothesis available.
  dec_trivial
end
def myeq {α : Type} (a b : α) : Prop := a = b

example {α : Type} (a b : α) (h : a = b) : myeq a b :=
begin
  success_if_fail { nontriviality α }, -- Fails
  nontriviality α using [myeq], -- There is now a `nontrivial α` hypothesis available
  assumption
end