logic.nontrivial - mathlib docs

@[class]

structure nontrivial (α : Type u_3) :

Prop

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. In vector spaces, this is equivalent to positive dimension.

Instances of this typeclass

source

theorem nontrivial_iff {α : Type u_1} :

nontrivial α ↔ ∃ (x y : α), x ≠ y

source

theorem exists_pair_ne (α : Type u_1) [nontrivial α] :

∃ (x y : α), x ≠ y

source

@[protected]

theorem decidable.exists_ne {α : Type u_1} [nontrivial α] [decidable_eq α] (x : α) :

∃ (y : α), y ≠ x

source

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

∃ (y : α), y ≠ x

source

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

nontrivial α

source

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

nontrivial α

source

theorem exists_pair_lt (α : Type u_1) [nontrivial α] [linear_order α] :

∃ (x y : α), x < y

source

theorem nontrivial_iff_lt {α : Type u_1} [linear_order α] :

nontrivial α ↔ ∃ (x y : α), x < y

source

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

nontrivial α ↔ ∃ (y : α), y ≠ x

source

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

nontrivial (subtype p) ↔ ∃ (y : α) (hy : p y), y ≠ ↑x

source

@[protected, instance]

def sort.nontrivial :

nontrivial Prop

source

@[protected, instance]

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

nonempty α

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.

source

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

psum (nontrivial α) (unique α)

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

Equations

nontrivial_psum_unique α = dite (nontrivial α) (λ (h : nontrivial α), psum.inl h) (λ (h : ¬nontrivial α), psum.inr {to_inhabited := {default := inhabited.default _inst_1}, uniq := _})

source

theorem subsingleton_iff {α : Type u_1} :

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

source

theorem not_nontrivial_iff_subsingleton {α : Type u_1} :

¬nontrivial α ↔ subsingleton α

source

theorem not_nontrivial (α : Type u_1) [subsingleton α] :

¬nontrivial α

source

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

¬subsingleton α

source

theorem subsingleton_or_nontrivial (α : Type u_1) :

subsingleton α ∨ nontrivial α

A type is either a subsingleton or nontrivial.

source

theorem false_of_nontrivial_of_subsingleton (α : Type u_1) [nontrivial α] [subsingleton α] :

false

source

@[protected, instance]

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

nontrivial (option α)

source

@[protected]

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.

source

@[protected]

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

nontrivial α

Pullback a nontrivial instance along a surjective function.

source

@[protected]

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.

source

@[protected, instance]

def nontrivial_prod_right {α : Type u_1} {β : Type u_2} [nonempty α] [nontrivial β] :

nontrivial (α × β)

source

@[protected, instance]

def 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

@[protected, instance]

def pi.nontrivial {I : Type u_3} {f : I → Type u_4} [inhabited I] [inst : ∀ (i : I), nonempty (f i)] [nontrivial (f inhabited.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

@[protected, instance]

def function.nontrivial {α : Type u_1} {β : Type u_2} [h : nonempty α] [nontrivial β] :

nontrivial (α → β)

source

meta def simp_attr.nontriviality :

(user_attribute simp_lemmas)

Simp lemmas for nontriviality tactic

source

@[protected]

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

x ≤ y

source

meta def tactic.nontriviality_by_elim (α : expr) (lems : interactive.parse tactic.simp_arg_list) :

tactic unit

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.

source

meta def tactic.nontriviality_by_assumption (α : expr) :

tactic unit

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

source

meta def tactic.interactive.nontriviality (t : interactive.parse (optional interactive.types.texpr)) (lems : interactive.parse (lean.parser.tk "using" *> tactic.simp_arg_list <|> has_pure.pure list.nil)) :

tactic unit

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
```

source

def tactic_doc.tactic.nontriviality :

tactic_doc_entry

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
```

source

@[protected, instance]

def bool.nontrivial :

nontrivial bool

mathlib documentation

Nontrivial types #