Nonempty.map2
theorem Nonempty.map2 :
∀ {α : Sort u_4} {β : Sort u_5} {γ : Sort u_6}, (α → β → γ) → Nonempty α → Nonempty β → Nonempty γ
This theorem states that for any three types `α`, `β`, and `γ`, given a function from `α` and `β` to `γ`, if `α` and `β` are nonempty, then `γ` is also nonempty. In mathematical terms, it says that if we have a function `f: α × β → γ` and we know that there exists at least one element in both `α` and `β`, then there exists at least one element in `γ`.
More concisely: If `α × β` is nonempty and `f: α × β → γ` is a function, then `γ` is nonempty.
|
Mathlib.Logic.Nonempty._auxLemma.6
theorem Mathlib.Logic.Nonempty._auxLemma.6 : ∀ {α : Sort u_4} {p : α → Prop}, Nonempty (Subtype p) = ∃ a, p a := by
sorry
This theorem states that for any type `α` and any property `p` that `α` might have, there exists a nonempty subtype of `α` that satisfies `p` if and only if there exists an element `a` of `α` that satisfies `p`. In other words, we can find a nonempty subtype of `α` with property `p` if we can find at least one instance of `α` that has property `p`.
More concisely: For any type `α` and property `p`, there exists a nonempty subtype of `α` with property `p` if and only if there exists an element `a` in `α` with property `p`.
|
nonempty_subtype
theorem nonempty_subtype : ∀ {α : Sort u_4} {p : α → Prop}, Nonempty (Subtype p) ↔ ∃ a, p a
The theorem `nonempty_subtype` states that for any type `α` and any predicate `p` on `α`, there exists a nonempty subtype `Subtype p` if and only if there exists an element `a` of `α` for which the predicate `p` holds true. Essentially, this theorem relates the existence of a nonempty subtype (a subset of a type where the elements satisfy a certain condition) to the existence of an element in the original type that satisfies the same condition.
More concisely: For any type `α` and predicate `p` on `α`, there exists a nonempty subtype `Subtype p` if and only if there exists an element `a` in `α` such that `p(a)` holds.
|
Nonempty.congr
theorem Nonempty.congr : ∀ {α : Sort u_4} {β : Sort u_5}, (α → β) → (β → α) → (Nonempty α ↔ Nonempty β)
This theorem, `Nonempty.congr`, states that for any two types `α` and `β`, if there exist functions from `α` to `β` and from `β` to `α`, then `α` is non-empty if and only if `β` is non-empty. In other words, if we can go back and forth between `α` and `β` via some functions, then the existence of an element in `α` is equivalent to the existence of an element in `β`.
More concisely: If types `α` and `β` have mutual inverses of functions between them, then `α` and `β` have the same non-emptiness property.
|
Nonempty.map
theorem Nonempty.map : ∀ {α : Sort u_4} {β : Sort u_5}, (α → β) → Nonempty α → Nonempty β
This theorem, referred to as "Nonempty.map", states that for any two types `α` and `β`, if there exists a function `f` that maps from `α` to `β`, and if `α` is nonempty (i.e., there exists at least one value of type `α`), then `β` is also nonempty. The comment also notes that `Nonempty` cannot be a `functor`, a concept in functional programming which maps between types, because in Lean, `Functor` is restricted to the `Type` sort.
More concisely: If `α` is a nonempty type and `f : α -> β` is a function, then `β` is a nonempty type.
|