Mathlib.Logic.Nontrivial.Basic

nontrivial_of_lt theorem

[Preorder α] (x y : α) (h : x < y) : Nontrivial α

Full source

theorem nontrivial_of_lt [Preorder α] (x y : α) (h : x < y) : Nontrivial α :=
  ⟨⟨x, y, ne_of_lt h⟩⟩

Nontriviality from Strict Order

Informal description

For any preorder $\alpha$ and elements $x, y \in \alpha$ such that $x < y$, the type $\alpha$ is nontrivial (i.e., contains at least two distinct elements).

exists_pair_lt theorem

(α : Type*) [Nontrivial α] [LinearOrder α] : ∃ x y : α, x < y

Full source

theorem exists_pair_lt (α : Type*) [Nontrivial α] [LinearOrder α] : ∃ x y : α, x < y := by
  rcases exists_pair_ne α with ⟨x, y, hxy⟩
  cases lt_or_gt_of_ne hxy <;> exact ⟨_, _, ‹_›⟩

Existence of Strictly Ordered Pair in Nontrivial Linearly Ordered Types

Informal description

For any nontrivial linearly ordered type $\alpha$, there exist two elements $x$ and $y$ in $\alpha$ such that $x < y$.

nontrivial_iff_lt theorem

[LinearOrder α] : Nontrivial α ↔ ∃ x y : α, x < y

Full source

theorem nontrivial_iff_lt [LinearOrder α] : NontrivialNontrivial α ↔ ∃ x y : α, x < y :=
  ⟨fun h ↦ @exists_pair_lt α h _, fun ⟨x, y, h⟩ ↦ nontrivial_of_lt x y h⟩

Nontriviality Criterion for Linearly Ordered Types via Strict Inequality

Informal description

For any linearly ordered type $\alpha$, $\alpha$ is nontrivial if and only if there exist two elements $x$ and $y$ in $\alpha$ such that $x < y$.

Subtype.nontrivial_iff_exists_ne theorem

(p : α → Prop) (x : Subtype p) : Nontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x

Full source

theorem Subtype.nontrivial_iff_exists_ne (p : α → Prop) (x : Subtype p) :
    NontrivialNontrivial (Subtype p) ↔ ∃ (y : α) (_ : p y), y ≠ x := by
  simp only [_root_.nontrivial_iff_exists_ne x, Subtype.exists, Ne, Subtype.ext_iff]

Nontriviality Criterion for Subtypes: $\text{Nontrivial }\{x \mid p(x)\} \leftrightarrow \exists y \neq x, p(y)$

Informal description

For any predicate $p$ on a type $\alpha$ and any element $x$ in the subtype defined by $p$, the subtype is nontrivial if and only if there exists an element $y \in \alpha$ satisfying $p(y)$ such that $y \neq x$.

nontrivialPSumUnique definition

(α : Type*) [Inhabited α] : Nontrivial α ⊕' Unique α

Full source

/-- An inhabited type is either nontrivial, or has a unique element. -/
noncomputable def nontrivialPSumUnique (α : Type*) [Inhabited α] :
    NontrivialNontrivial α ⊕' Unique α :=
  if h : Nontrivial α then PSum.inl h
  else
    PSum.inr
      { default := default,
        uniq := fun x : α ↦ by
          by_contra H
          exact h ⟨_, _, H⟩ }

Nontrivial or Unique Inhabited Type

Informal description

For any inhabited type $\alpha$, either $\alpha$ is nontrivial (contains at least two distinct elements) or $\alpha$ has a unique element (i.e., is a singleton).

Option.nontrivial instance

[Nonempty α] : Nontrivial (Option α)

Full source

instance Option.nontrivial [Nonempty α] : Nontrivial (Option α) := by
  inhabit α
  exact ⟨none, some default, nofun⟩

Nontriviality of Optional Values

Informal description

For any nonempty type $\alpha$, the type of optional values `Option α` is nontrivial (contains at least two distinct elements).

Function.Injective.nontrivial theorem

[Nontrivial α] {f : α → β} (hf : Function.Injective f) : Nontrivial β

Full source

/-- Pushforward a `Nontrivial` instance along an injective function. -/
protected theorem Function.Injective.nontrivial [Nontrivial α] {f : α → β}
    (hf : Function.Injective f) : Nontrivial β :=
  let ⟨x, y, h⟩ := exists_pair_ne α
  ⟨⟨f x, f y, hf.ne h⟩⟩

Injective Functions Preserve Nontriviality

Informal description

If $\alpha$ is a nontrivial type and $f : \alpha \to \beta$ is an injective function, then $\beta$ is also a nontrivial type.

Function.Injective.exists_ne theorem

[Nontrivial α] {f : α → β} (hf : Function.Injective f) (y : β) : ∃ x, f x ≠ y

Full source

/-- An injective function from a nontrivial type has an argument at
which it does not take a given value. -/
protected theorem Function.Injective.exists_ne [Nontrivial α] {f : α → β}
    (hf : Function.Injective f) (y : β) : ∃ x, f x ≠ y := by
  rcases exists_pair_ne α with ⟨x₁, x₂, hx⟩
  by_cases h : f x₂ = y
  · exact ⟨x₁, (hf.ne_iff' h).2 hx⟩
  · exact ⟨x₂, h⟩

Existence of Non-Image Element for Injective Functions on Nontrivial Types

Informal description

Let $\alpha$ be a nontrivial type and $f \colon \alpha \to \beta$ be an injective function. Then for any element $y \in \beta$, there exists an element $x \in \alpha$ such that $f(x) \neq y$.

nontrivial_prod_right instance

[Nonempty α] [Nontrivial β] : Nontrivial (α × β)

Full source

instance nontrivial_prod_right [Nonempty α] [Nontrivial β] : Nontrivial (α × β) :=
  Prod.snd_surjective.nontrivial

Nontriviality of Product Types (Right Factor)

Informal description

For any nonempty type $\alpha$ and nontrivial type $\beta$, the product type $\alpha \times \beta$ is also nontrivial.

nontrivial_prod_left instance

[Nontrivial α] [Nonempty β] : Nontrivial (α × β)

Full source

instance nontrivial_prod_left [Nontrivial α] [Nonempty β] : Nontrivial (α × β) :=
  Prod.fst_surjective.nontrivial

Nontriviality of Product Types (Left Factor)

Informal description

For any nontrivial type $\alpha$ and nonempty type $\beta$, the product type $\alpha \times \beta$ is also nontrivial.

Pi.nontrivial_at theorem

(i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] : Nontrivial (∀ i : I, f i)

Full source

/-- A pi type is nontrivial if it's nonempty everywhere and nontrivial somewhere. -/
theorem nontrivial_at (i' : I) [inst : ∀ i, Nonempty (f i)] [Nontrivial (f i')] :
    Nontrivial (∀ i : I, f i) := by
  letI := Classical.decEq (∀ i : I, f i)
  exact (Function.update_injective (fun i ↦ Classical.choice (inst i)) i').nontrivial

Nontriviality of Dependent Function Type at a Point

Informal description

Let $I$ be a type, and for each $i \in I$, let $f(i)$ be a nonempty type. If there exists an index $i' \in I$ such that $f(i')$ is a nontrivial type, then the dependent function type $\forall i : I, f(i)$ is also nontrivial.

Pi.nontrivial instance

[Inhabited I] [∀ i, Nonempty (f i)] [Nontrivial (f default)] : Nontrivial (∀ i : I, f i)

Full source

/-- 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 nontrivial [Inhabited I] [∀ i, Nonempty (f i)] [Nontrivial (f default)] :
    Nontrivial (∀ i : I, f i) :=
  nontrivial_at default

Nontriviality of Dependent Function Type at Default Index

Informal description

For any inhabited type $I$ and a family of nonempty types $f(i)$ indexed by $I$, if the type $f(\text{default})$ is nontrivial, then the dependent function type $\forall i : I, f(i)$ is also nontrivial.

Function.nontrivial instance

[h : Nonempty α] [Nontrivial β] : Nontrivial (α → β)

Full source

instance Function.nontrivial [h : Nonempty α] [Nontrivial β] : Nontrivial (α → β) :=
  h.elim fun a ↦ Pi.nontrivial_at a

Nontriviality of Function Types

Informal description

For any nonempty type $\alpha$ and nontrivial type $\beta$, the function type $\alpha \to \beta$ is also nontrivial.

Subsingleton.le theorem

[Preorder α] [Subsingleton α] (x y : α) : x ≤ y

Full source

@[nontriviality]
protected theorem Subsingleton.le [Preorder α] [Subsingleton α] (x y : α) : x ≤ y :=
  le_of_eq (Subsingleton.elim x y)

Subsingleton Preorder Elements are Comparable

Informal description

For any preorder $\alpha$ that is a subsingleton (i.e., all elements are equal), any two elements $x$ and $y$ in $\alpha$ satisfy $x \leq y$.