Prod.exists
theorem Prod.exists : ∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∃ x, p x) ↔ ∃ a b, p (a, b)
This theorem states that for all types `α` and `β` and a property `p` applied to pairs of elements from `α` and `β`, there exists an element that satisfies `p` if and only if there exist separate elements `a` from `α` and `b` from `β` such that the pair `(a, b)` satisfies `p`. In other words, it shows the equivalence between finding a pair that satisfies a property and finding individual elements from each type that make up a pair satisfying the same property.
More concisely: For all types `α` and `β` and properties `p` on pairs from `α × β`, the existence of a pair `(a, b)` satisfying `p` is equivalent to the existence of separate elements `a ∈ α` and `b ∈ β` such that `p(a, b)` holds.
|
Function.Surjective.Prod_map
theorem Function.Surjective.Prod_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
Function.Surjective f → Function.Surjective g → Function.Surjective (Prod.map f g)
The theorem `Function.Surjective.Prod_map` states that for any four types `α`, `β`, `γ` and `δ` and any two functions `f` from `α` to `γ` and `g` from `β` to `δ`, if `f` and `g` are both surjective functions, then the function `Prod.map f g`, which applies `f` to the first component and `g` to the second component of a pair (from type `α × β` to type `γ × δ`), is also surjective. In other words, for every pair in the codomain `γ × δ`, there exists a pair in the domain `α × β` such that applying the function `Prod.map f g` to the pair from the domain produces the pair from the codomain.
More concisely: If `f` from `α` to `γ` and `g` from `β` to `δ` are surjective functions, then the function `Prod.map f g` from `α × β` to `γ × δ` is also surjective.
|
Prod.map_map
theorem Prod.map_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ)
(g : β → ε) (g' : δ → ζ) (x : α × γ), Prod.map g g' (Prod.map f f' x) = Prod.map (g ∘ f) (g' ∘ f') x
The theorem `Prod.map_map` states that for all types α, β, γ, δ, ε, and ζ and for functions `f` mapping from α to β, `f'` from γ to δ, `g` from β to ε, `g'` from δ to ζ, and for any pair `x` of type α × γ, the composition of two `Prod.map` functions is equivalent to a single application of `Prod.map` using the composition of the corresponding functions. In other words, applying `Prod.map` with `g` and `g'` to the result of `Prod.map` with `f` and `f'` applied to `x` is the same as applying `Prod.map` with `g ∘ f` and `g' ∘ f'` directly to `x`.
More concisely: For all types α, β, γ, δ, ε, and ζ, and functions f : α → β, f' : γ → δ, g : β → ε, g' : δ → ζ, the function Prod.map (g × g') (f × f') equals Prod.map (g ∘ f) (g' ∘ f').
|
Mathlib.Data.Prod.Basic._auxLemma.1
theorem Mathlib.Data.Prod.Basic._auxLemma.1 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) = ∀ (a : α) (b : β), p (a, b)
This theorem, `Mathlib.Data.Prod.Basic._auxLemma.1`, states that for all types `α` and `β`, and for any property `p` that applies to pairs of type `α × β`, stating that the property `p` holds for every pair `x` of type `α × β` is equivalent to stating that for every element `a` of type `α` and every element `b` of type `β`, the property `p` holds for the pair `(a, b)`. In other words, it relates the universal quantification over a product type to universal quantifications over each of the components.
More concisely: For any property `p` and types `α` and `β`, the statement "for all `x` in `α × β`, `p x` holds" is equivalent to "for all `a` in `α` and `b` in `β`, `p (a, b)` holds."
|
Prod.fst_surjective
theorem Prod.fst_surjective : ∀ {α : Type u_1} {β : Type u_2} [h : Nonempty β], Function.Surjective Prod.fst
The theorem `Prod.fst_surjective` states that for all types `α` and `β`, given that `β` is nonempty, the first projection function `Prod.fst` is surjective. In other words, for every element of `α` in the product type `α × β`, there exists a pair in `α × β` such that when we apply the `Prod.fst` function (which extracts the first element of the pair), we can get any element of `α`. This means that we can reach every element of `α` by selecting some pair from `α × β` and taking its first component.
More concisely: For any nonempty type `β`, the first projection function `Prod.fst` of the product type `α × β` is a surjection from `α`.
|
Prod.forall
theorem Prod.forall :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∀ (x : α × β), p x) ↔ ∀ (a : α) (b : β), p (a, b)
This theorem states that for any two types `α` and `β`, and a property `p` that applies to a pair of elements (one from each type), the statement "for all pairs `(a, b)`, `p (a, b)` holds true" is equivalent to "for all pairs `x`, `p x` holds true". In other words, it says that the property holds for all pairs in the Cartesian product of the two types, regardless of how we express the pair.
More concisely: For any types `α` and `β` and property `p` on pairs `(α × β) → Prop`, the statements "for all `(a, b)`, `p a b` hold true" and "for all `x`, `p x.fst x.snd` hold true" are equivalent.
|
Prod.mk.eta
theorem Prod.mk.eta : ∀ {α : Type u_1} {β : Type u_2} {p : α × β}, (p.1, p.2) = p
This theorem, named `Prod.mk.eta`, states that for any pair `p` of arbitrary type `α` and `β`, the pair formed by taking the first and second elements of `p`, i.e. `(p.1, p.2)`, is equal to the original pair `p`. In simple terms, it demonstrates the property of reconstructing a pair from its components without any loss of information.
More concisely: For any pair `p` of type `α × β`, the tuple `(p.1, p.2)` is equal to `p`.
|
Prod.ext_iff
theorem Prod.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {p q : α × β}, p = q ↔ p.1 = q.1 ∧ p.2 = q.2
The theorem `Prod.ext_iff` states that for any two pairs `p` and `q`, from any two types `α` and `β`, `p` is equal to `q` if and only if the first element of `p` is equal to the first element of `q` and the second element of `p` is equal to the second element of `q`. Essentially, it provides the condition for equality of two pairs in a product type.
More concisely: For any pairs p and q of types α × β, p = q if and only if p.1 = q.1 and p.2 = q.2.
|
Prod.swap_swap
theorem Prod.swap_swap : ∀ {α : Type u_1} {β : Type u_2} (x : α × β), x.swap.swap = x
This theorem, named `Prod.swap_swap`, states that for all types `α` and `β`, and for any pair `x` of type `α × β`, applying the `Prod.swap` function twice to `x` (i.e., swapping the elements of the pair twice) results in the original pair `x`. In other words, the double application of the `Prod.swap` function is an identity operation on the pair `x`.
More concisely: For all types `α` and `β`, the repeated application of `Prod.swap` to a pair `x` of type `α × β` results in the original pair `x`: `Prod.swap (Prod.swap x) = x`.
|
Prod.map_comp_map
theorem Prod.map_comp_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ)
(g : β → ε) (g' : δ → ζ), Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')
The theorem `Prod.map_comp_map` asserts that for all types `α`, `β`, `γ`, `δ`, `ε`, and `ζ`, and for all functions `f : α → β`, `f' : γ → δ`, `g : β → ε`, and `g' : δ → ζ`, the composition of `Prod.map g g'` with `Prod.map f f'` is equivalent to a single `Prod.map` of the composed functions `(g ∘ f)` and `(g' ∘ f')`. In other words, it encapsulates the principle that mapping over a product type (a pair of values) is compatible with function composition.
More concisely: For all functions f : α → β, g : β → ε, f' : γ → δ, and g' : δ → ζ, the map operations commute with function composition, that is, Prod.map (g ∘ f) (f' x, g' y) = Prod.map f (f' x) ∗ Prod.map g (g' y).
|
Prod.swap_leftInverse
theorem Prod.swap_leftInverse : ∀ {α : Type u_1} {β : Type u_2}, Function.LeftInverse Prod.swap Prod.swap
The theorem `Prod.swap_leftInverse` states that for any two types `α` and `β`, the `Prod.swap` operation (which swaps the elements in a pair) is its own left inverse. This means that performing `Prod.swap` twice on any pair will return the original pair. In formal terms, given any pair `(a, b)` of elements from `α` and `β` respectively, applying `Prod.swap` twice results in `(a, b)`. This can be expressed concisely as `Prod.swap ∘ Prod.swap = id` where `id` is the identity function.
More concisely: For all types `α` and `β`, the `Prod.swap` operation on pairs of elements from `α` and `β` is idempotent, i.e., `Prod.swap ∘ Prod.swap = id`.
|
Prod.mk.inj_iff
theorem Prod.mk.inj_iff :
∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
This theorem states that for any two pairs of elements, where the elements in each pair are from possibly different types (`α` and `β`), the two pairs are equal if and only if the elements at corresponding positions in the pairs are equal. In terms of mathematical notation, given two pairs `(a₁, b₁)` and `(a₂, b₂)` - where `a₁`, `a₂` are of type `α` and `b₁`, `b₂` are of type `β` - the pairs are equal (i.e., `(a₁, b₁) = (a₂, b₂)`) if and only if `a₁ = a₂` and `b₁ = b₂`.
More concisely: Given pairs `(a:_,_)` and `(b:_,_)` of elements where the first components have type `α` and the second components have type `β`, the pairs are equal if and only if their first components are equal and their second components are equal. (or equivalently, `(a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂`)
|
Function.Injective.Prod_map
theorem Function.Injective.Prod_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
Function.Injective f → Function.Injective g → Function.Injective (Prod.map f g)
The theorem `Function.Injective.Prod_map` states that for any four types `α`, `β`, `γ`, `δ` and two functions `f : α → γ` and `g : β → δ`, if function `f` is injective and function `g` is also injective, then the function `Prod.map f g` is also injective. Here, `Prod.map f g` is a function that applies `f` to the first component and `g` to the second component of a pair from the Cartesian product of `α` and `β`. In mathematical terms, an injective function (or one-to-one function) is a function that maps distinct elements of its domain to distinct elements of its codomain. Hence, the theorem essentially states that the injectivity property is preserved under the operation of forming Cartesian products with functions.
More concisely: If functions `f : α → γ` and `g : β → δ` are injective, then the function `Prod.map f g` that maps `(x, y)` to `(f x, g y)` is also injective.
|
Function.LeftInverse.Prod_map
theorem Function.LeftInverse.Prod_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f₁ : α → β} {g₁ : γ → δ} {f₂ : β → α} {g₂ : δ → γ},
Function.LeftInverse f₁ f₂ →
Function.LeftInverse g₁ g₂ → Function.LeftInverse (Prod.map f₁ g₁) (Prod.map f₂ g₂)
This theorem asserts that for any four types `α`, `β`, `γ` and `δ`, and for any functions `f₁ : α → β`, `g₁ : γ → δ`, `f₂ : β → α`, and `g₂ : δ → γ`, if `f₁` is a left inverse to `f₂` and `g₁` is a left inverse to `g₂`, then the function `Prod.map f₁ g₁` is a left inverse to the function `Prod.map f₂ g₂`. In other words, if reversing the operations of `f₁` and `g₁` with `f₂` and `g₂` respectively leads us back to the original value, then applying this to pairs of values, with `f₁` and `g₁` applied to the first and second elements of the pair respectively, will also lead us back to the original pair when the operations are reversed.
More concisely: If functions `f₁ : α → β`, `g₁ : γ → δ`, `f₂ : β → α`, and `g₂ : δ → γ` satisfy `f₁ ∘ f₂ = id α` and `g₁ ∘ g₂ = id δ`, then `g₁ ∘ f₂ = id (α × γ)`. (Here, `id` denotes the identity function, and `α × γ` denotes the product type of `α` and `γ`.)
|
Prod.mk.inj_left
theorem Prod.mk.inj_left : ∀ {α : Type u_5} {β : Type u_6} (a : α), Function.Injective (Prod.mk a)
The theorem `Prod.mk.inj_left` states that for any type `α` and `β` and for any given element `a` of type `α`, the function `Prod.mk a` is injective. In other words, if we fix an element `a : α` and consider the function that takes an element `b : β` to the pair `(a, b)`, then different inputs `b` will always produce different pairs `(a, b)`. This function, `Prod.mk a`, is thus injective.
More concisely: For any type `α` and element `a` of type `α`, the function mapping `β` to the pair `(a, β)` is an injection.
|
Prod.swap_injective
theorem Prod.swap_injective : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective Prod.swap
This theorem states that for any types `α` and `β`, the function `Prod.swap` is injective. In other words, for any pairs of elements `(a, b)` and `(c, d)` from the Cartesian product of the types `α` and `β`, if `Prod.swap (a, b) = Prod.swap (c, d)` (meaning that `(b, a) = (d, c)`), then it must be the case that `(a, b) = (c, d)`. This essentially means that swapping the elements of a pair doesn't create any duplicate pairs, hence the function `Prod.swap` is injective.
More concisely: For any types `α` and `β`, the function `Prod.swap` on the Cartesian product `α × β` is a bijection. (Injectivity is half of this statement, and the surjectivity part states that for any `(c, d)` in `α × β`, there exists a unique `(a, b)` such that `Prod.swap (a, b) = (c, d)`.)
|
Mathlib.Data.Prod.Basic._auxLemma.2
theorem Mathlib.Data.Prod.Basic._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} {p : α × β → Prop}, (∃ x, p x) = ∃ a b, p (a, b)
This theorem states that for any types `α` and `β`, and any property `p` pertaining to an ordered pair of elements from `α` and `β`, the assertion that there exists an ordered pair satisfying property `p` is logically equivalent to the assertion that there exist elements `a` from `α` and `b` from `β` such that the ordered pair `(a, b)` satisfies property `p`. In other words, it formalizes the intuitive idea that saying "there exists a pair which has property `p`" is the same as saying "there exists an `a` and a `b` such that the pair `(a, b)` has property `p`".
More concisely: For any types `α` and `β` and property `p` on ordered pairs of `α × β`, the existence of an ordered pair in `α × β` satisfying `p` is equivalent to the existence of elements `a` from `α` and `b` from `β` such that `(a, b)` satisfies `p`.
|
Prod.mk.inj_right
theorem Prod.mk.inj_right : ∀ {α : Type u_5} {β : Type u_6} (b : β), Function.Injective fun a => (a, b)
The theorem `Prod.mk.inj_right` states that for all types `α` and `β`, and for any given value `b` of type `β`, the function that takes an input `a` of type `α` and pairs it with `b` to form a tuple `(a, b)` is injective. In other words, if this function maps two different inputs from `α` to the same tuple `(a, b)`, then those two inputs must have been the same to begin with. This is a particular case of injectivity where the second component of the tuple is kept constant.
More concisely: For any types `α` and `β`, the function that maps `α` to the tuple `(-, b)` with a fixed `β` value `b` is an injection.
|
Prod.snd_surjective
theorem Prod.snd_surjective : ∀ {α : Type u_1} {β : Type u_2} [h : Nonempty α], Function.Surjective Prod.snd
This theorem states that for any types `α` and `β`, given that `α` is nonempty, the second projection function `Prod.snd` is surjective. In other words, for any element `b` of type `β`, there exists a pair in the product type `α × β` such that 'b' is the second component of the pair. This is expressed by the function `Prod.snd`, which takes a pair and returns its second component.
More concisely: For any nonempty type `α` and type `β`, the second projection function `Prod.snd` of `α × β` is surjective, i.e., for every `b` in `β`, there exists `(a, b)` in `α × β`.
|
Prod.map_id
theorem Prod.map_id : ∀ {α : Type u_1} {β : Type u_2}, Prod.map id id = id
The theorem `Prod.map_id` states that for any pair of types `α` and `β`, applying the `Prod.map` function with `id` (the identity function) for both components results in the identity function. In other words, if we map each component of a pair (from `α` and `β` respectively) with the identity function, we get back the original pair. This is akin to saying that the identity function leaves all elements of the pair unchanged.
More concisely: For any types `α` and `β`, `Prod.map id (x, y) = (x, y)`.
|
Prod.map_def
theorem Prod.map_def :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
Prod.map f g = fun p => (f p.1, g p.2)
The theorem `Prod.map_def` states that for any types `α`, `β`, `γ`, and `δ` and any functions `f : α → γ` and `g : β → δ`, the function `Prod.map f g` is the same as the function that takes a pair `p` and returns a new pair, where the first element is the result of applying `f` to the first element of `p` and the second element is the result of applying `g` to the second element of `p`, i.e., `(f p.1, g p.2)`. In other words, `Prod.map` applies `f` to the first component and `g` to the second component of a pair, as its name suggests.
More concisely: For functions `f : α → γ` and `g : β → δ`, `Prod.map f g` equals the function that maps a pair `(x, y)` to `(f x, g y)`.
|