Unique.uniq
theorem Unique.uniq : ∀ {α : Sort u} (self : Unique α) (a : α), a = default
This theorem states that for any type `α` that is 'Unique', every term of type `α` is equal to the default element of that type (from the `Inhabited` typeclass). In other words, if we consider `α` as a 'Unique' type, then we can take any element 'a' of type `α`, and it will always equal the default value. In mathematical terms, it asserts the uniqueness property of elements in a 'Unique' type.
More concisely: For any Unique type `α`, every element `a:` α is equal to the default element of `α`.
|
Option.subsingleton_iff_isEmpty
theorem Option.subsingleton_iff_isEmpty : ∀ {α : Type u}, Subsingleton (Option α) ↔ IsEmpty α
This theorem states that an `Option` type over a type `α` (notated as `Option α`) is a `Subsingleton` if and only if `α` is an empty type. In other words, there can only be at most one distinct value of `Option α` (which is the definition of a `Subsingleton`) if and only if there are no values of `α` (which is the definition of `IsEmpty`). This theorem allows us to infer the emptiness of a type based on the subsingularity of its corresponding `Option` type, and vice versa.
More concisely: The option type `Option α` is a subsingleton if and only if type `α` is empty.
|
Unique.forall_iff
theorem Unique.forall_iff : ∀ {α : Sort u_1} [inst : Unique α] {p : α → Prop}, (∀ (a : α), p a) ↔ p default
This theorem states that for any sort `α`, given that `α` has a unique instance, and considering a property `p` that applies to all elements of `α`, it is equivalent to say that `p` holds for all elements of `α` and to say that `p` holds for the default element of `α`. In other words, if there's only one instance of a sort, proving a property about all instances is the same as proving it about the default instance.
More concisely: For any sort `α` with a unique instance and property `p`, proving `p` for all elements of `α` is equivalent to proving `p` for the default element of `α`.
|
Function.Injective.subsingleton
theorem Function.Injective.subsingleton :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.Injective f → ∀ [inst : Subsingleton β], Subsingleton α := by
sorry
The theorem states that if we have an injective function (a function where different inputs always produce different outputs) from one set to another, and if the set that is the function's output (the codomain) is a subsingleton (a set with at most one element), then the set that is the function's input (the domain) must also be a subsingleton. In other words, if a function cannot produce the same output from two different inputs, and there is at most one possible output, then there can be at most one possible input.
More concisely: If a function from a set to a subsingleton set is injective, then the set is a subsingleton.
|
Unique.default_eq
theorem Unique.default_eq : ∀ {α : Sort u_1} [inst : Unique α] (a : α), default = a
This theorem states that for any type `α` (which could be a type or a proposition) and any instance of `α` named 'a', if `α` has a unique instance, then the default instance of `α` is equal to 'a'. In other words, if a type has exactly one instance, then any element of that type is necessarily equal to the default instance.
More concisely: If type `α` has a unique instance 'a, then `α.default` equals 'a.
|
Unique.eq_default
theorem Unique.eq_default : ∀ {α : Sort u_1} [inst : Unique α] (a : α), a = default
Given any type α (which is of sort `u_1`) and an instance of `Unique α` (which means that there is exactly one object of type α), the theorem `Unique.eq_default` states that any object `a` of type α is equal to the default object of type α. In other words, for a unique type, any object of that type must be the default object.
More concisely: For any unique type α, any of its objects is equal to the default object.
|
Function.Surjective.subsingleton
theorem Function.Surjective.subsingleton :
∀ {α : Sort u_1} {β : Sort u_2} {f : α → β} [inst : Subsingleton α], Function.Surjective f → Subsingleton β := by
sorry
This theorem states that if a function `f` from `α` to `β` is surjective (i.e. for every element `b` in `β`, there exists some element `a` in `α` such that `f(a) = b`), and if `α` is a subsingleton (i.e., `α` has at most one element), then `β` is also a subsingleton. In other words, if we have a surjective function whose domain contains at most one element, then its codomain must also contain at most one element.
More concisely: If a surjective function maps a subsingleton domain to a codomain, then the codomain is also a subsingleton.
|