Mathlib.Logic.IsEmpty._auxLemma.2
theorem Mathlib.Logic.IsEmpty._auxLemma.2 : ∀ {α : Sort u_1} [inst : IsEmpty α] {p : α → Prop}, (∃ a, p a) = False := by
sorry
This theorem states that for any sort `α` that is empty (as specified by the `IsEmpty` typeclass), and for any proposition `p` that depends on elements of `α`, the proposition "there exists an element in `α` such that `p` holds for that element" is always false. Essentially, this is because there can't be any elements in `α` for `p` to hold for, as `α` is empty.
More concisely: For any empty sort `α` and proposition `p` depending on elements of `α`, ∀ (a : α), ¬ p(a) holds.
|
Mathlib.Logic.IsEmpty._auxLemma.19
theorem Mathlib.Logic.IsEmpty._auxLemma.19 :
∀ {α : Type u_1} {β : Type u_2}, Nonempty (α × β) = (Nonempty α ∧ Nonempty β)
This theorem, `Mathlib.Logic.IsEmpty._auxLemma.19`, states that for any type `α` and any predicate `p` on `α`, the subtype of `α` for which `p` holds is empty if and only if for every element `x` of `α`, `p x` is not true. Basically, it links the emptiness of a subtype defined by a certain property to the absence of that property in the entire type.
More concisely: For any type `α` and predicate `p` on `α`, the subtype of `α` where `p` holds is empty if and only if `p` does not hold for any element in `α`.
|
Mathlib.Logic.IsEmpty._auxLemma.4
theorem Mathlib.Logic.IsEmpty._auxLemma.4 : ∀ {α : Sort u_1}, (¬IsEmpty α) = Nonempty α
This theorem from the Mathlib.Logic.IsEmpty library states that for any type `α`, the negation of `α` being empty is equivalent to `α` being nonempty. In other words, if it is not the case that there are zero elements of type `α`, then there must exist at least one element of type `α`.
More concisely: The negation of a type being empty is equivalent to it being nonempty.
|
Subtype.isEmpty_of_false
theorem Subtype.isEmpty_of_false : ∀ {α : Sort u_1} {p : α → Prop}, (∀ (a : α), ¬p a) → IsEmpty (Subtype p)
This theorem states that if there is a predicate `p` that is false for all elements `a` of a certain type `α`, then the subtype of `α` defined by `p` is empty. In other words, there are no elements in type `α` that satisfy the predicate `p`. This is a theorem about type theory and logic in Lean 4 theorem prover.
More concisely: If a predicate `p` is universally false over a type `α`, then the subtype of `α` defined by `p` is empty.
|
Mathlib.Logic.IsEmpty._auxLemma.5
theorem Mathlib.Logic.IsEmpty._auxLemma.5 : ∀ {α : Sort u_1}, IsEmpty α = ¬Nonempty α
This theorem states that for any kind `α` (which can be a type or a sort), `α` is empty if and only if it is not nonempty. In other words, the property of being empty for a type is logically equivalent to the negation of the property of being nonempty for that type. Here, `IsEmpty α` means that there are no elements of type `α`, and `Nonempty α` means that there exists at least one element of type `α`.
More concisely: For any type `α`, `IsEmpty α` is equivalent to `∥α∥ = ∅`, where `∥_∥` denotes the size or the cardinality of a type. In other words, a type is empty if and only if it has no elements.
|
isEmpty_iff
theorem isEmpty_iff : ∀ {α : Sort u_1}, IsEmpty α ↔ α → False
This theorem, `isEmpty_iff`, states that for any type `α`, the type is `IsEmpty` (i.e., it has no elements) if and only if any function from `α` to `False` (i.e., a function that can't be defined because it can't produce any outputs given inputs from `α`). In other words, a type is empty if there is no possible way to construct an element of that type, which is equivalent to saying there can be no function that produces a `False` value from an element of that type because such elements don't exist.
More concisely: A type `α` is empty if and only if there exists no function from `α` to `False`.
|
Mathlib.Logic.IsEmpty._auxLemma.1
theorem Mathlib.Logic.IsEmpty._auxLemma.1 :
∀ {α : Sort u_1} [inst : IsEmpty α] {p : α → Prop}, (∀ (a : α), p a) = True
This theorem states that for any sort `α` which is empty (i.e., there are no elements of type `α`), and for any property `p` that elements of `α` might have, the statement "for all `a` in `α`, `p(a)` holds" is always true. This is a manifestation of the principle of vacuous truth in logic: statements about all elements of an empty set are trivially true because there are no elements to contradict them.
More concisely: If `α` is an empty sort, then the proposition `∀a:α, p(a)` is true for any property `p`.
|
not_nonempty_iff
theorem not_nonempty_iff : ∀ {α : Sort u_1}, ¬Nonempty α ↔ IsEmpty α
This theorem states that for any type `α`, the proposition that `α` is not nonempty is equivalent to `α` being empty. Here, `Nonempty α` represents that there exists an element of type `α` and `IsEmpty α` denotes that there are no elements of type `α`. So, this theorem connects the negation of existence with the non-existence in the context of types in Lean 4.
More concisely: The proposition that a type `α` has no elements is equivalent to `α` being empty.
|
Function.isEmpty
theorem Function.isEmpty : ∀ {α : Sort u_1} {β : Sort u_2} [inst : IsEmpty β], (α → β) → IsEmpty α
This theorem is stating that if for any types `α` and `β`, if `β` is an empty type (i.e., has no values), then any function from `α` to `β` implies that `α` is also an empty type. In other words, if there are no values in `β` to map to, then there can't be any values in `α` either. This theorem is a statement about the impossibility to define a function from some type `α` to an empty type `β`.
More concisely: If `β` is an empty type, then any function from a non-empty type `α` to `β` implies `α` is empty.
|
Mathlib.Logic.IsEmpty._auxLemma.3
theorem Mathlib.Logic.IsEmpty._auxLemma.3 : ∀ {α : Sort u_1}, (¬Nonempty α) = IsEmpty α
This theorem states that for any type `α`, the property that `α` is not nonempty (`¬Nonempty α`) is equivalent to the property that `α` is empty (`IsEmpty α`). In other words, if there are no elements of a given type `α`, then that type is considered empty. This theorem provides a formal equivalence between the negative statement of nonemptiness and the assertion of emptiness in the context of Lean's type theory.
More concisely: The theorem asserts that the type `α` is empty if and only if it is not nonempty in Lean's type theory.
|
Mathlib.Logic.IsEmpty._auxLemma.14
theorem Mathlib.Logic.IsEmpty._auxLemma.14 :
∀ {α : Type u_5} {E : α → Type u_4}, IsEmpty (Sigma E) = ∀ (a : α), IsEmpty (E a)
This theorem states that for any type `α` and any property `p` of the elements of `α`, the statement "there does not exist an element `x` in `α` such that `p(x)` holds" is equivalent to the statement "for all elements `x` in `α`, `p(x)` does not hold". In mathematical notation, this can be expressed as "¬∃x, p(x) = ∀x, ¬p(x)".
More concisely: The negation of the existence of an element in a type with a given property is equivalent to the universally quantified negation of that property holding for all elements. (i.e., ¬∃x. P(x) ≤f=≄> ∀x. ¬P(x))
|
isEmpty_or_nonempty
theorem isEmpty_or_nonempty : ∀ (α : Sort u_1), IsEmpty α ∨ Nonempty α
This theorem, named `isEmpty_or_nonempty`, states that for any sort (a type or a proposition) `α`, `α` is either `IsEmpty` (i.e., it has no elements) or `Nonempty` (i.e., it has at least one element). In other words, a given type or proposition cannot simultaneously be empty and nonempty.
More concisely: For any type or proposition `α`, `α` is either empty or nonempty.
|
not_isEmpty_iff
theorem not_isEmpty_iff : ∀ {α : Sort u_1}, ¬IsEmpty α ↔ Nonempty α
This theorem states that for any type `α`, it is not the case that `α` is empty if and only if `α` is nonempty. In other words, a type `α` is not empty if there exists at least one element of type `α`. Conversely, if `α` is nonempty, then it cannot be the case that `α` is empty.
More concisely: A type `α` is nonempty if and only if it is not empty.
|
isEmpty_sum
theorem isEmpty_sum : ∀ {α : Type u_4} {β : Type u_5}, IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β
This theorem, `isEmpty_sum`, states that for any two types `α` and `β`, the type `α ⊕ β` (which denotes the sum type, or the disjoint union of `α` and `β`) is empty if and only if both `α` and `β` are empty. Here, `IsEmpty` is a predicate that checks whether a type has no values.
More concisely: The sum type `α ⊕ β` is empty if and only if types `α` and `β` are both empty.
|