Nontrivial types #
Results about Nontrivial.
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
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 := ⋯ }
Instances For
theorem
Function.Injective.nontrivial
{α : Type u_1}
{β : Type u_2}
[Nontrivial α]
{f : α → β}
(hf : Function.Injective f)
:
Pushforward a Nontrivial instance along an injective 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.
instance
nontrivial_prod_right
{α : Type u_1}
{β : Type u_2}
[Nonempty α]
[Nontrivial β]
:
Nontrivial (α × β)
Equations
- ⋯ = ⋯
instance
nontrivial_prod_left
{α : Type u_1}
{β : Type u_2}
[Nontrivial α]
[Nonempty β]
:
Nontrivial (α × β)
Equations
- ⋯ = ⋯
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.
Equations
- ⋯ = ⋯
instance
Function.nontrivial
{α : Type u_1}
{β : Type u_2}
[h : Nonempty α]
[Nontrivial β]
:
Nontrivial (α → β)
Equations
- ⋯ = ⋯