Mathlib.Data.Set.Prod._auxLemma.7
theorem Mathlib.Data.Set.Prod._auxLemma.7 : ∀ {a b c : Prop}, (a ∧ b ∧ c) = (b ∧ a ∧ c)
This theorem states that for any three propositions `a`, `b`, and `c`, the conjunction of `a`, `b`, and `c` in the order `a ∧ b ∧ c` is logically equivalent to the conjunction of these propositions in the order `b ∧ a ∧ c`. In other words, the order in which the propositions are joined with "and" does not change the truth of the overall statement.
More concisely: The theorem asserts that for any propositions `a`, `b`, and `c`, the conjunctions `a ∧ b ∧ c` and `b ∧ a ∧ c` are logically equivalent.
|
Set.prod_subset_preimage_snd
theorem Set.prod_subset_preimage_snd :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), s ×ˢ t ⊆ Prod.snd ⁻¹' t
This theorem states that for any two sets `s` and `t`, where `s` is a set of type `α` and `t` is a set of type `β`, the Cartesian product of `s` and `t` (`s ×ˢ t`) is a subset of the preimage of `t` under the function `Prod.snd`. In other words, every pair `(a, b)` in the Cartesian product, where `a` is from `s` and `b` is from `t`, maps to an element in `t` under the function `Prod.snd`, which extracts the second component of the pair.
More concisely: For all sets `α` and `β`, the image of the Cartesian product `s × t` under the second projection `Prod.snd` is contained in `t`.
|
Mathlib.Data.Set.Prod._auxLemma.13
theorem Mathlib.Data.Set.Prod._auxLemma.13 :
∀ {α : Type u} {β : Type v} {s : Set α} {t : Set β} {p : α × β}, (p ∈ s ×ˢ t) = (p.1 ∈ s ∧ p.2 ∈ t)
This theorem, named `Mathlib.Data.Set.Prod._auxLemma.13`, states that for any two sets `s` of type `α` and `t` of type `β`, and any ordered pair `p` of type `α × β`, the pair `p` is a member of the Cartesian product of `s` and `t` if and only if the first element of `p` is a member of `s` and the second element of `p` is a member of `t`. In mathematical terms, it asserts that $(p \in s \times t) \iff (p_1 \in s \land p_2 \in t)$.
More concisely: The theorem asserts that for any sets `s` and `t`, and any pair `p` in their Cartesian product `s × t`, the first component `p.1` is in `s` and the second component `p.2` is in `t`. In symbols: for all `s : Type _, t : Type _, p : s × t, p = (x, y) ↔ x ∈ s ∧ y ∈ t`.
|
Set.mk_preimage_prod
theorem Set.mk_preimage_prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : γ → α) (g : γ → β),
(fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t
This theorem, `Set.mk_preimage_prod`, states that for any three types `α`, `β`, and `γ`, any two sets `s` of type `α` and `t` of type `β`, and any two functions `f` and `g` from `γ` to `α` and `β` respectively, the preimage of set `s` cross `t` under the function that pairs the results of `f` and `g` applied on an element is equal to the intersection of the preimages of set `s` under `f` and set `t` under `g`. This theorem relates the concept of preimage of a function with the operations of set intersection and cartesian product.
More concisely: For any sets `s` of type `α`, `t` of type `β`, and functions `f: γ -> α` and `g: γ -> β`, the preimage of `s` x `t` under the function that pairs `f` and `g` is equal to the intersection of `f^(-1)(s)` and `g^(-1)(t)`.
|
Set.prod_inter
theorem Set.prod_inter :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t₁ t₂ : Set β}, s ×ˢ (t₁ ∩ t₂) = s ×ˢ t₁ ∩ s ×ˢ t₂
This theorem, `Set.prod_inter`, states that for any two types `α` and `β`, a set `s` of type `α`, and two sets `t₁` and `t₂` of type `β`, the Cartesian product of `s` with the intersection of `t₁` and `t₂` is equal to the intersection of the Cartesian product of `s` with `t₁` and the Cartesian product of `s` with `t₂`. In more mathematical terms, for sets \(s\), \(t_1\), \(t_2\), we have \(s \times (t_1 \cap t_2) = (s \times t_1) \cap (s \times t_2)\).
More concisely: For any sets `α`, `β`, `s : Set α`, and `t₁`, `t₂ : Set β`, `Set.prod_inter` asserts that `s × (t₁ ∩ t₂) = (s × t₁) ∩ (s × t₂)`.
|
Set.prod_subset_preimage_fst
theorem Set.prod_subset_preimage_fst :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), s ×ˢ t ⊆ Prod.fst ⁻¹' s
This theorem states that for any two sets `s` of arbitrary type `α` and `t` of arbitrary type `β`, the cartesian product of `s` and `t` (denoted as `s ×ˢ t` in Lean), is a subset of the preimage of `s` under the function `Prod.fst`.
In other words, for all pairs `(a, b)` in the cartesian product of `s` and `t`, the first element `a` of the pair is in set `s`. `Prod.fst` is a function that takes a pair and returns its first element. The expression `Prod.fst ⁻¹' s` represents the preimage of `s` under `Prod.fst`, that is, all pairs `(a, b)` such that `a` belongs to `s`.
More concisely: For any sets `s` of type `α` and `t` of type `β`, the cartesian product `s × Catalisate t` is a subset of the preimage `(⁺» Prod.fst <$> s)` of `s` under the function `Prod.fst`. (In Lean notation)
Or in more traditional mathematical notation:
For all `(a, b)` in `s × t`, `a` is an element of `s`.
|
Set.prod_univ
theorem Set.prod_univ : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s ×ˢ Set.univ = Prod.fst ⁻¹' s
The theorem `Set.prod_univ` states that for any type `α` and `β`, and any set `s` of type `α`, the cartesian product of `s` and the universal set of `β` is precisely the preimage of `s` under the first projection function. In other words, if you take all pairs whose first element is in the set `s` and second element is in the universal set of `β`, this is equivalent to all elements in `s`. This theorem provides a useful identity in dealing with cartesian products involving the universal set.
More concisely: For any type `α` and `β`, and set `s` of type `α`, the cartesian product `s × β` is equal to the preimage of `s` under the first projection function.
|
Set.range_diag
theorem Set.range_diag : ∀ {α : Type u_1}, (Set.range fun x => (x, x)) = Set.diagonal α
This theorem states that for any type `α`, the range of the function that maps each element `x` of `α` to the pair `(x, x)` is exactly the diagonal set of `α`. In other words, it says that the set of all pairs `(x, x)` where `x` is an element from `α` (which is what we call the diagonal set of `α`) is exactly the same as the set of all possible outputs (range) of the function that takes any `x` in `α` and pairs it with itself.
More concisely: The diagonal set of a type `α` equals the range of the function that maps each element `x` in `α` to the pair `(x, x)`.
|
Set.univ_prod_univ
theorem Set.univ_prod_univ : ∀ {α : Type u_1} {β : Type u_2}, Set.univ ×ˢ Set.univ = Set.univ
This theorem states that the Cartesian product of the universal set on type `α` and the universal set on type `β` (denoted as `Set.univ ×ˢ Set.univ`) is also a universal set. In other words, the Cartesian product of all elements of two arbitrary types `α` and `β` includes every possible pair from `α` and `β`, which forms a new universal set. This theorem holds for any types `α` and `β`.
More concisely: The Cartesian product of the universal sets on types `α` and `β` is itself a universal set.
|
Set.subset_pi_eval_image
theorem Set.subset_pi_eval_image :
∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) (u : Set ((i : ι) → α i)), u ⊆ s.pi fun i => Function.eval i '' u
The theorem `Set.subset_pi_eval_image` states that for any set `s` of indices `ι`, and any set `u` of dependent functions from `ι` to some types `α i`, the set `u` is a subset of the set of dependent functions `f : Πa, π a` such that for each index `i` in `s`, `f i` belongs to the image of the function `Function.eval i` applied to `u`. In other words, for each function in `u`, each of its evaluations at indices in `s` is still in the image of `u` under the evaluation at that index.
More concisely: For any set `s` of indices `ι` and dependent functions `u : Πi, α i`, `u` is a subset of the set of functions `f : Πa, π a` such that for all `i` in `s`, `f i` is in the image of `Function.eval i` applied to `u`.
|
Set.pi_mono
theorem Set.pi_mono :
∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
(∀ i ∈ s, t₁ i ⊆ t₂ i) → s.pi t₁ ⊆ s.pi t₂
The theorem `Set.pi_mono` states that for any type `ι`, any function `α` from `ι` to some type, any set `s` of `ι`, and any two families of sets `t₁` and `t₂` (indexed by `ι` and mapping to sets of elements of the type determined by `α`), if every set in the `t₁` family is a subset of the corresponding set in the `t₂` family for each index in `s`, then the set of dependent functions that belongs to every set in the `t₁` family (whenever the index is in `s`) is a subset of the set of dependent functions that belongs to every set in the `t₂` family (whenever the index is in `s`). In other words, it provides a condition under which one can assert that one set of dependent functions is a subset of another.
More concisely: If for any family of sets `t₁` and `t₂` indexed by a type `ι`, and any set `s ⊆ ι`, every set in `t₁` is a subset of the corresponding set in `t₂` for indices in `s`, then the set of dependent functions belonging to sets in `t₁` for indices in `s` is a subset of the set of dependent functions belonging to sets in `t₂` for indices in `s`.
|
Set.Nonempty.prod
theorem Set.Nonempty.prod :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s.Nonempty → t.Nonempty → (s ×ˢ t).Nonempty
The theorem `Set.Nonempty.prod` asserts that for any two types `α` and `β`, and sets `s` of type `α` and `t` of type `β`, if `s` and `t` are both nonempty (i.e., each contains at least one element), then the Cartesian product of `s` and `t`, denoted `s ×ˢ t`, is also nonempty. In other words, it's not possible to create a Cartesian product from two sets where one or both of them are empty.
More concisely: If `α` and `β` are types, and `s : Set α` and `t : Set β` are nonempty, then `s ×ˢ t` is a nonempty set.
|
Set.singleton_prod_singleton
theorem Set.singleton_prod_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β}, {a} ×ˢ {b} = {(a, b)} := by
sorry
This theorem states that for any two types `α` and `β` and any elements `a` of `α` and `b` of `β`, the Cartesian product of the set containing only `a` and the set containing only `b` (`{a} ×ˢ {b}` in Lean 4) is equal to the set containing only the pair `(a, b)`. This is a statement about set theory in the context of type theory.
More concisely: For any types `α` and `β` and their respective elements `a` from `α` and `b` from `β`, `{a} × {b} = {(a, b)}`.
|
Set.singleton_pi
theorem Set.singleton_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} (i : ι) (t : (i : ι) → Set (α i)), {i}.pi t = Function.eval i ⁻¹' t i := by
sorry
The theorem `Set.singleton_pi` states that for any type `ι`, any function `α` mapping elements of `ι` to types, any element `i` of `ι`, and any function `t` mapping elements of `ι` to sets of the corresponding type `α`, the set of dependent functions `f` such that `f a` belongs to `t a` for each `a` in the singleton set `{i}`, is equal to the preimage of the set `t i` under the function `Function.eval i`. In other words, it's the set of functions `f` that map `i` to an element in `t i`.
More concisely: For any type `ι`, function `α : ι → Type`, element `i` of `ι`, and set `t : ι → Set`, the function `{f : ι → α // ∀ a, f a ∈ t a}`, which selects functions mapping `i` to an element in `t i`, is equal to the set `{g : α | g ∈ t i ∧ ∀ a, a = i → g = f a}`.
|
Set.prod_mono
theorem Set.prod_mono :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ ×ˢ t₁ ⊆ s₂ ×ˢ t₂
The theorem `Set.prod_mono` states that for any types `α` and `β`, and any sets `s₁`, `s₂` of type `α` along with `t₁`, `t₂` of type `β`, if `s₁` is a subset of `s₂` and `t₁` is a subset of `t₂`, then the cartesian product of `s₁` and `t₁` is also a subset of the cartesian product of `s₂` and `t₂`. In mathematical terms, given $s₁, s₂ \subseteq \alpha$ and $t₁, t₂ \subseteq \beta$, if $s₁ \subseteq s₂$ and $t₁ \subseteq t₂$, then $s₁ \times t₁ \subseteq s₂ \times t₂$.
More concisely: If `s₁ ⊆ s₂` and `t₁ ⊆ t₂`, then `s₁ × t₁ ⊆ s₂ × t₂`. (In mathematical notation: for any types `α` and `β`, if `s₁, s₂ ⊆ α` and `t₁, t₂ ⊆ β`, then `s₁ × t₁ ⊆ s₂ × t₂`. )
|
Set.prod_empty
theorem Set.prod_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s ×ˢ ∅ = ∅
This theorem states that for any type `α` and `β` and any set `s` of type `α`, the cartesian product of set `s` and an empty set is always an empty set. In other words, if you form pairs where the first element comes from set `s` and the second element comes from an empty set, you'll end up with an empty set, because there are no elements to select from the empty set.
More concisely: For any set `s`, the cartesian product `s × {}` is an empty set.
|
Set.prod_range_range_eq
theorem Set.prod_range_range_eq :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ},
Set.range m₁ ×ˢ Set.range m₂ = Set.range fun p => (m₁ p.1, m₂ p.2)
The theorem `Set.prod_range_range_eq` states that for any types `α`, `β`, `γ`, and `δ` and any functions `m₁` mapping from `α` to `γ` and `m₂` mapping from `β` to `δ`, the cartesian product of the ranges of `m₁` and `m₂` is equal to the range of the function that takes a pair `(p.1, p.2)` and maps it to `(m₁ p.1, m₂ p.2)`. In other words, if you create all possible pairs from the outputs of `m₁` and `m₂`, it's the same as if you first pair up the inputs and then apply `m₁` to the first element and `m₂` to the second.
More concisely: The ranges of functions `m₁ : α → γ` and `m₂ : β → δ` are equal as sets, that is, `{(m₁ x, m₂ y) | x ∈ α, y ∈ β} = {(a, b) | (x, y) ∈ α × β, a = m₁ x, b = m₂ y}`.
|
Mathlib.Data.Set.Prod._auxLemma.26
theorem Mathlib.Data.Set.Prod._auxLemma.26 : ∀ {a b c : Prop}, (a ∨ b → c) = ((a → c) ∧ (b → c))
This theorem, named `Mathlib.Data.Set.Prod._auxLemma.26`, states that for any three propositions `a`, `b`, and `c`, the statement "`a` OR `b` implies `c`" is logically equivalent to the combined statements "`a` implies `c`" AND "`b` implies `c`". This is a basic result from propositional logic expressed in the language of Lean 4.
More concisely: The theorem `Mathlib.Data.Set.PropositionalLogic.or_imp_distrib` in Lean 4 states that for all propositions `a`, `b`, and `c`, `(a Orleans b) -> c` is logically equivalent to `(a -> c)` and `(b -> c)`.
|
Set.singleton_prod
theorem Set.singleton_prod : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {a : α}, {a} ×ˢ t = Prod.mk a '' t
The theorem `Set.singleton_prod` states that for any types `α` and `β`, any set `t` of type `β`, and any element `a` of type `α`, the Cartesian product of the singleton set containing `a` and the set `t` is equal to the image of the set `t` under the function `Prod.mk a`. In mathematical terms, this means that for all `a` in `α` and all sets `t` of elements of `β`, we have {a} × t = {(a, b) | b ∈ t}, where × denotes the Cartesian product and {(a, b) | b ∈ t} is the set of all pairs (a, b) with b in `t`.
More concisely: For any types `α` and `β`, and for any `a ∈ α` and set `t ∈ β`, the singleton set {`a`} and set `t` have the same Cartesian product, that is, {`a`} × `t` = {(`a`, `b`) | `b ∈ t`}.
|
Set.empty_prod
theorem Set.empty_prod : ∀ {α : Type u_1} {β : Type u_2} {t : Set β}, ∅ ×ˢ t = ∅
The theorem `Set.empty_prod` states that for all types `α` and `β`, and for any set `t` of type `β`, the cartesian product of the empty set (denoted by `∅`) and `t` is equal to the empty set. In mathematical notation, this could be written as `∅ × t = ∅`. This theorem reflects the idea that if you form pairs where one component must come from an empty set, you can't form any pairs, resulting in an empty set.
More concisely: The empty set taken as a factor in a cartesian product results in an empty set for any set as the second factor. (i.e., ∅ × t = ∅)
|
Set.snd_image_prod
theorem Set.snd_image_prod :
∀ {α : Type u_1} {β : Type u_2} {s : Set α}, s.Nonempty → ∀ (t : Set β), Prod.snd '' s ×ˢ t = t
The theorem `Set.snd_image_prod` states that for any types `α` and `β`, given a set `s` of type `α` which is nonempty, and any set `t` of type `β`, the image under the second projection function (`Prod.snd`) of the cartesian product of `s` and `t` is equal to `t`. In other words, if we take each pair in the cartesian product of `s` and `t` and map it to its second element, we get the set `t` back. It is a statement about the property and behavior of the second projection function (`Prod.snd`) when acting on the cartesian product of two sets, where one of the sets is nonempty.
More concisely: For any nonempty set `s` and set `t`, the image of the cartesian product `s × t` under the second projection function `Prod.snd` is equal to `t`.
|
Set.Nonempty.fst
theorem Set.Nonempty.fst : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty → s.Nonempty := by
sorry
The theorem `Set.Nonempty.fst` states that for any types `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, if the Cartesian product of `s` and `t` (`s ×ˢ t`) is nonempty, then the set `s` is also nonempty. In other words, having at least one pair of elements from `s` and `t` implies that `s` must contain at least one element.
More concisely: If the Cartesian product of sets `s` and `t` is nonempty, then `s` is nonempty.
|
Set.preimage_swap_prod
theorem Set.preimage_swap_prod :
∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Prod.swap ⁻¹' s ×ˢ t = t ×ˢ s
The theorem `Set.preimage_swap_prod` states that for any two sets `s` of type `α` and `t` of type `β`, the preimage of the Cartesian product of `s` and `t` under the swapping function is the same as the Cartesian product of `t` and `s`. In other words, if you take the Cartesian product of `s` and `t`, swap the elements in each pair, and then take the preimage under the swapping function, the result will be the same as if you had just taken the Cartesian product of `t` and `s` directly. This theorem demonstrates the interchangeability of the factors of a Cartesian product under the swap operation. This can be expressed in mathematical terms as: for all sets `s` and `t`, $(\mathrm{swap}^{-1}(s \times t)) = t \times s$.
More concisely: For any sets `s` and `t`, swapping the factors of their Cartesian product and taking the preimage is equal to directly taking the Cartesian product of `t` and `s`, i.e., $(\mathrm{swap}^{-1}(s \times t)) = t \times s$.
|
Set.inter_prod
theorem Set.inter_prod :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β}, (s₁ ∩ s₂) ×ˢ t = s₁ ×ˢ t ∩ s₂ ×ˢ t
The theorem `Set.inter_prod` states that for any types `α` and `β`, and for any sets `s₁`, `s₂` of type `α`, and a set `t` of type `β`, the Cartesian product of the intersection of `s₁` and `s₂` with `t` is equal to the intersection of the Cartesian product of `s₁` with `t` and the Cartesian product of `s₂` with `t`. In mathematical terms, this can be expressed as (s₁ ∩ s₂) × t = (s₁ × t) ∩ (s₂ × t), where × represents the Cartesian product and ∩ represents the intersection of sets.
More concisely: For any types `α`, sets `s₁`, `s₂`, and `t` of types `α`, the Cartesian product of the intersection of `s₁` and `s₂` with `t` equals the intersection of the Cartesian products of `s₁` and `t`, and `s₂` and `t`.
|
Mathlib.Data.Set.Prod._auxLemma.50
theorem Mathlib.Data.Set.Prod._auxLemma.50 : ∀ {α : Type u} (x : α), (x ∈ ∅) = False
This theorem states that for any index set `ι`, family of sets `t` indexed by `ι`, set `s` of indices from `ι`, and a function `f` that maps each element `i` in `ι` to an element in `α i`, the function `f` belongs to the set `Set.pi s t` (i.e., `f` is one of the dependent functions described by `Set.pi s t`) if and only if for all `i` in `s`, `f(i)` belongs to `t i`. In other words, `f` is in `Set.pi s t` exactly when `f` maps each index in `s` to an element within the corresponding set in the family `t`.
More concisely: A function `f` belongs to `Set.pi s t` in Lean 4 if and only if for all `i` in `s`, `f(i)` is an element of `t(i)`.
|
Mathlib.Data.Set.Prod._auxLemma.3
theorem Mathlib.Data.Set.Prod._auxLemma.3 : ∀ {a b c : Prop}, ((a ∧ b) ∧ c) = (a ∧ b ∧ c)
This theorem states that for any three propositions `a`, `b`, and `c`, the statement "a and b and c" is logically equivalent to the statement "a and (b and c)". In other words, the logical conjunction operator, represented by `∧`, is associative. This means that the order in which the conjunctions are performed does not change the truth value of the whole expression.
More concisely: The logical conjunction operation is associative, that is, `a ∧ (b ∧ c)` is equivalent to `(a ∧ b) ∧ c` for any propositions `a`, `b`, and `c`.
|
injective_toPullbackDiag
theorem injective_toPullbackDiag : ∀ {X : Type u_1} {Y : Sort u_2} (f : X → Y), Function.Injective (toPullbackDiag f)
This theorem states that for all types `X` and `Y`, and for any function `f` from `X` to `Y`, the function `toPullbackDiag f` is injective. This means that if `toPullbackDiag f` maps two elements from `X` to the same element in the pullback of `f` with itself, then those two elements must be identical. In other words, `toPullbackDiag f` never maps different elements to the same value, when `f` is a function from `X` to `Y`. Here, `toPullbackDiag f` is the diagonal map from `X` to the pullback of `f` with itself, which associates to each element `x` of `X` the pair `(x, x)` in the pullback, satisfying some property.
More concisely: For any function `f` from type `X` to type `Y`, the diagonal map `toPullbackDiag f` from `X` to the pullback of `f` with itself is an injection.
|
Set.Subsingleton.offDiag_eq_empty
theorem Set.Subsingleton.offDiag_eq_empty : ∀ {α : Type u_1} {s : Set α}, s.Nontrivial → s.offDiag.Nonempty
This theorem, referred to as an **Alias** of the reverse direction of `Set.offDiag_nonempty`, states that for any set `s` of a certain type `α`, if `s` is non-trivial (i.e., it contains at least two distinct elements), then the off-diagonal of `s` is non-empty. The "off-diagonal" of a set refers to the collection of pairs of distinct elements from that set. So in other words, the theorem says that if a set has at least two different elements, then it's possible to form at least one pair of different elements from that set.
More concisely: If a set of type `α` contains at least two distinct elements, then its off-diagonal is non-empty.
|
Set.univ_pi_update
theorem Set.univ_pi_update :
∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] {β : ι → Type u_4} (i : ι) (f : (j : ι) → α j) (a : α i)
(t : (j : ι) → α j → Set (β j)),
(Set.univ.pi fun j => t j (Function.update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j => t j (f j)
This theorem, `Set.univ_pi_update`, states that for any types `ι` and `α : ι → Type`, given a function `f` from `ι` to `α`, an element `i` of `ι`, a value `a` of `α i`, and a family of sets `t` indexed by `ι`, the set of all functions `x` such that `x` equals the updated function at `i` and belongs to the set `t j (Function.update f i a j)` for all `j`, is equal to the intersection of the set `{x | x i ∈ t i a}` and the set of all functions that do not equal `i` and belong to the set `t j (f j)` for all such `j`. Essentially, it describes how updating the value of a function at a particular point affects the corresponding dependent product of sets.
More concisely: The set of functions updating a given function at a specific index with a new value and belonging to a family of sets for all other indices is equal to the intersection of the set of functions agreeing with the updated value at the index and the set of functions agreeing with the original values at all other indices in the family.
|
Set.prod_nonempty_iff
theorem Set.prod_nonempty_iff :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
This theorem, `Set.prod_nonempty_iff`, states that for any two types `α` and `β`, and any two sets `s` of type `α` and `t` of type `β`, the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is nonempty if and only if both `s` and `t` are nonempty. In other words, there exists an element in the Cartesian product of the two sets exactly when there exist elements in both of the original sets.
More concisely: For any types `α` and `β` and sets `s : α` and `t : β`, `s ×ˢ t` is nonempty if and only if `s` and `t` are nonempty.
|
Mathlib.Data.Set.Prod._auxLemma.8
theorem Mathlib.Data.Set.Prod._auxLemma.8 : ∀ {α : Sort u_1} {a b : α}, (a = b) = (b = a)
This theorem, from the Mathlib library and specifically from the Data.Set.Prod module, states that for all types `α` and for all elements `a` and `b` of that type, the statement that `a` equals `b` is equivalent to the statement that `b` equals `a`. In other words, it asserts the symmetry of equality: if `a` equals `b`, then `b` equals `a`, and vice versa.
More concisely: The theorem asserts the symmetry of equality: for all types `α` and all elements `a` and `b` of type `α`, `a = b` is equivalent to `b = a`.
|
Set.eval_image_univ_pi
theorem Set.eval_image_univ_pi :
∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)} {i : ι},
(Set.univ.pi t).Nonempty → (fun f => f i) '' Set.univ.pi t = t i
This theorem states that for any index type `ι`, any indexed type `α`, any function `t` from `ι` to the set of elements of `α`, and any index `i` of type `ι`, if the set of all functions from `ι` to `α` (where, for each index `i` in the universal set, the function's value at `i` lies in `t i`) is nonempty, then the image of this set of functions under the function that maps each function to its value at `i` is equal to `t i`. In essence, if you have a nonempty set of functions and you apply each function to a specific index, you get exactly the set of all possible values at that index.
More concisely: If `t : ι → α` and the set of functions from `ι` to `α` with values in `t` at each index is nonempty, then `{f ι | ∀ i, f i ∈ t} = t i`.
|
Set.prod_self_subset_prod_self
theorem Set.prod_self_subset_prod_self : ∀ {α : Type u_1} {s₁ s₂ : Set α}, s₁ ×ˢ s₁ ⊆ s₂ ×ˢ s₂ ↔ s₁ ⊆ s₂
This theorem states that for any type `α` and any sets `s₁` and `s₂` of this type, the cartesian product of `s₁` with itself is a subset of the cartesian product of `s₂` with itself if and only if `s₁` is a subset of `s₂`. Here, the cartesian product of two sets `s₁` and `s₂` is a set of ordered pairs, each consisting of one element from `s₁` and one element from `s₂`. A subset relationship between two sets implies that any element of the first set is also an element of the second set.
More concisely: For any types `α` and sets `s₁` and `s₂` of type `α`, `s₁ × s₁ ⊆ s₂ × s₂` if and only if `s₁ ⊆ s₂`. Here, `×` denotes the cartesian product of sets.
|
Set.range_prod_map
theorem Set.range_prod_map :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {m₁ : α → γ} {m₂ : β → δ},
Set.range (Prod.map m₁ m₂) = Set.range m₁ ×ˢ Set.range m₂
This theorem, `Set.range_prod_map`, states that for any two functions `m₁` mapping from type `α` to `γ` and `m₂` mapping from type `β` to `δ`, the range of the function produced by mapping `m₁` and `m₂` across a pair, that is `Prod.map m₁ m₂`, is equal to the cartesian product of the range of `m₁` and the range of `m₂`. In mathematical terms, if we denote the range of a function `f` as `Range(f)`, then `Range(Prod.map m₁ m₂) = Range(m₁) × Range(m₂)`. This result illustrates how the range of a function that operates on pairs relates to the ranges of its component functions.
More concisely: The range of the function `Prod.map m₁ m₂` over the product type `α × β` is equal to the cartesian product of the ranges of `m₁` over `α` and `m₂` over `β`.
|
Set.union_prod
theorem Set.union_prod :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t : Set β}, (s₁ ∪ s₂) ×ˢ t = s₁ ×ˢ t ∪ s₂ ×ˢ t
The theorem `Set.union_prod` states that for any types `α` and `β`, any sets `s₁` and `s₂` of type `α`, and any set `t` of type `β`, the cartesian product of the union of `s₁` and `s₂` with `t` is equal to the union of the cartesian product of `s₁` with `t` and the cartesian product of `s₂` with `t`. In other words, it expresses a distributive property of the cartesian product operation over the union operation in the context of sets. Mathematically, this can be written as: $(s₁ ∪ s₂) × t = (s₁ × t) ∪ (s₂ × t)$.
More concisely: The cartesian product of the union of two sets with a third set is equal to the union of the cartesian products of each pair of sets.
|
Set.pi_congr
theorem Set.pi_congr :
∀ {ι : Type u_1} {α : ι → Type u_2} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
s₁ = s₂ → (∀ i ∈ s₁, t₁ i = t₂ i) → s₁.pi t₁ = s₂.pi t₂
The theorem `Set.pi_congr` states that for any index set `ι`, and any two families of sets `s₁, s₂` indexed by `ι`, and any two families of sets `t₁, t₂` whose types are indexed by elements in `s₁` or `s₂`, if `s₁` equals `s₂` and for any element `i` in `s₁`, the set `t₁ i` equals the set `t₂ i`, then the dependent function sets `Set.pi s₁ t₁` and `Set.pi s₂ t₂` are equal. In simpler terms, this theorem is about the equality of two sets of functions: if the indexing sets and the dependent sets are the same for two sets of functions, then the sets of functions themselves are equal.
More concisely: If two indexed families of sets have equal indices and equal sets for each index, then their corresponding dependent function sets are equal.
|
Set.univ_prod
theorem Set.univ_prod : ∀ {α : Type u_1} {β : Type u_2} {t : Set β}, Set.univ ×ˢ t = Prod.snd ⁻¹' t
The theorem `Set.univ_prod` states that for any types `α` and `β`, and any set `t` of elements of type `β`, the Cartesian product of the universal set of type `α` and set `t` is equivalent to the preimage of set `t` under the function `Prod.snd`. In simpler terms, it means that the set of all pairs (from `α` and `t`) is the same as the set of all second elements from `t`.
More concisely: The Cartesian product of the universal set of type `α` and a set `t` of type `β` is equal to the image of `t` under the second projection `Prod.snd`.
|
Set.univ_pi_eq_empty_iff
theorem Set.univ_pi_eq_empty_iff :
∀ {ι : Type u_1} {α : ι → Type u_2} {t : (i : ι) → Set (α i)}, Set.univ.pi t = ∅ ↔ ∃ i, t i = ∅
This theorem states that for any given type `ι` and a family of sets `t` where each set is of type `α i` for some `i` in `ι`, the set of all dependent functions from `ι` to `α i` (denoted by `Set.pi Set.univ t`) is empty if and only if there exists an `i` such that the corresponding set `t i` is empty. In other words, the Cartesian product of all sets in the family `t` is empty if and only if at least one of the sets in the family is empty.
More concisely: The set of dependent functions from a type `ι` to a family `t` of sets `α i` is empty if and only if one of the sets `t i` is empty. (Equivalently, the Cartesian product of the sets in `t` is non-empty if and only if all sets in `t` are non-empty.)
|
Mathlib.Data.Set.Prod._auxLemma.12
theorem Mathlib.Data.Set.Prod._auxLemma.12 : ∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∩ b) = (x ∈ a ∧ x ∈ b) := by
sorry
This theorem, titled `Mathlib.Data.Set.Prod._auxLemma.12`, states that for all types `α`, given an element `x` of this type and two sets `a` and `b` of the same type, the condition of `x` being in the intersection of set `a` and set `b` (denoted as `x ∈ a ∩ b`) is equivalent to `x` being in set `a` and `x` being in set `b` at the same time (denoted as `x ∈ a ∧ x ∈ b`). In other words, the membership of an element in the intersection of two sets is equivalent to the membership of the element in both of the sets separately.
More concisely: For all types `α` and sets `a` and `b` of type `α`, the element `x` is in the intersection `a ∩ b` if and only if `x` is in `a` and `x` is in `b`.
|
Set.pi_univ
theorem Set.pi_univ : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι), (s.pi fun i => Set.univ) = Set.univ
This theorem, `Set.pi_univ`, states that for any index set `ι` and a family of types `α` indexed by `ι`, and for any set `s` of `ι`, the set of all dependent functions from `ι` to `α` that map every element of `s` to the universal set is itself the universal set. In other words, if every element of the set `s` is mapped to the set containing every possible value of the type, then the set of all these functions is the set of all possible functions.
More concisely: For any index set `ι` and a family of types `α`, the set of dependent functions from `ι` to `α` that map each element of a subset `s` of `ι` to the universal set `Set.univ` equals the universal set.
|
Mathlib.Data.Set.Prod._auxLemma.32
theorem Mathlib.Data.Set.Prod._auxLemma.32 : ∀ (p : Prop), (True ∧ p) = p
This theorem states that for any proposition `p`, the statement `p or False` is equivalent to `p` itself. This makes sense in the realm of logic because "or" is a truth-functional operator, so if one of the operands is `False`, the overall truth of the statement depends on the other operand. In this case, `p or False` simplifies to just `p`.
More concisely: For all propositions p, p or False is logically equivalent to p.
|
Mathlib.Data.Set.Prod._auxLemma.46
theorem Mathlib.Data.Set.Prod._auxLemma.46 : ∀ {α : Type u_1} {s : Set α}, (s.offDiag = ∅) = s.Subsingleton
This theorem states that for any type `α` and a set `s` of type `α`, the property that the off-diagonal of set `s` is nonempty is equivalent to the property that the set `s` is nontrivial. In mathematical terms, a set is nonempty if it contains at least one element, and it is nontrivial if it contains at least two distinct elements. The "off-diagonal" of a set refers to the set of all pairs `(a, b)` where `a` and `b` are elements of the set and `a` is not equal to `b`. Therefore, the theorem is saying that the set `s` has at least two distinct elements if and only if there exist two elements in `s` that are not equal to each other.
More concisely: A set is nonempty and has at least two distinct elements if and only if its off-diagonal is nonempty.
|
Set.prod_singleton
theorem Set.prod_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {b : β}, s ×ˢ {b} = (fun a => (a, b)) '' s
The `Set.prod_singleton` theorem in Lean 4 states that for any set `s` of a particular type `α`, and any element `b` of another type `β`, the Cartesian product of `s` and the set containing only `b` (`s ×ˢ {b}`) is equal to the image of `s` under the function that pairs each element of `s` with `b` (`(fun a => (a, b)) '' s`). In other words, it states that the set of all pairs where the first element is from `s` and the second element is `b`, is the same as the set of all pairs generated by applying the pairing function to each element of `s`.
More concisely: The Cartesian product of a set `s` with a singleton set `{b}` is equal to the image of `s` under the function that pairs each element of `s` with `b`.
|
Mathlib.Data.Set.Prod._auxLemma.5
theorem Mathlib.Data.Set.Prod._auxLemma.5 :
∀ {α : Sort u_1} {p q : α → Prop}, (∀ (x : α), p x ∧ q x) = ((∀ (x : α), p x) ∧ ∀ (x : α), q x)
This theorem states that, for any type `α` and any two predicates `p` and `q` defined on `α`, the assertion that every element of `α` satisfies both `p` and `q` is equivalent to the assertion that every element of `α` satisfies `p` and every element of `α` satisfies `q`. In other words, if `p` and `q` are properties that elements of `α` might have, then the claim "every element of `α` has both properties `p` and `q`" is the same as the claim "every element of `α` has property `p` and every element of `α` has property `q`".
More concisely: For any type `α` and predicates `p` and `q` on `α`, the proposition `∀x : α, p x ∧ q x` is equivalent to `∀x : α, p x ∧ q x`. (In Lean syntax, `∧` represents logical and.)
|
Set.offDiag_nonempty
theorem Set.offDiag_nonempty : ∀ {α : Type u_1} {s : Set α}, s.offDiag.Nonempty ↔ s.Nontrivial
The theorem `Set.offDiag_nonempty` states that for any set `s` of a certain type `α`, the off-diagonal of `s` is nonempty if and only if `s` is nontrivial. Here, the off-diagonal of `s` is defined as the set of all pairs `(a, b)` such that `a` and `b` are in `s` and `a` is not equal to `b`. A set `s` is said to be nontrivial if it contains at least two distinct elements. So, in essence, the theorem states that a set has at least two distinct elements if and only if there exist two elements in the set that form a pair in the off-diagonal.
More concisely: A set of type `α` has a nonempty off-diagonal if and only if it contains at least two distinct elements.
|
Set.singleton_pi'
theorem Set.singleton_pi' :
∀ {ι : Type u_1} {α : ι → Type u_2} (i : ι) (t : (i : ι) → Set (α i)), {i}.pi t = {x | x i ∈ t i}
The theorem `Set.singleton_pi'` states that for any type `ι`, any function `α : ι → Type u_2`, any element `i : ι`, and any family of sets `t : (i : ι) → Set (α i)`, the set of dependent functions `f : Πa, π a` such that `f a` belongs to `t a` whenever `a` is in the singleton set `{i}`, is the same as the set of functions `x` where `x i` belongs to `t i`. In other words, when considering only the functions defined at a single point `i`, the condition for a function to be in the set of functions is simply that its value at `i` is in the corresponding set `t i`.
More concisely: For any type `ι`, function `α : ι → Type u_2`, element `i : ι`, and set family `t : (i : ι) → Set (α i)`, the dependent functions in `Πa, π a` with `f a ∈ t a` for `a` in the singleton set `{i}` are identical to the functions `x` with `x i ∈ t i`.
|
Set.Nontrivial.offDiag_nonempty
theorem Set.Nontrivial.offDiag_nonempty : ∀ {α : Type u_1} {s : Set α}, s.Nontrivial → s.offDiag.Nonempty
This theorem, known as `Set.Nontrivial.offDiag_nonempty`, states that for any set `s` of a certain type `α`, if the set `s` is nontrivial (i.e., there exist two distinct elements in the set), then the set of off-diagonal elements of `s` is nonempty. The off-diagonal set of a set `s` is the set of pairs `(a, b)` such that `a` and `b` are distinct elements of `s`. Thus, the theorem essentially says that a nontrivial set contains at least one pair of distinct elements.
More concisely: If a set of type `α` contains at least two distinct elements, then its set of off-diagonal pairs is nonempty.
|
Set.prod_subset_iff
theorem Set.prod_subset_iff :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {P : Set (α × β)},
s ×ˢ t ⊆ P ↔ ∀ x ∈ s, ∀ y ∈ t, (x, y) ∈ P
The theorem `Set.prod_subset_iff` states that for any types `α` and `β`, and for any sets `s` of type `α`, `t` of type `β`, and `P` of type `(α × β)`, the Cartesian product of `s` and `t` is a subset of `P` if and only if for every element `x` in `s` and every element `y` in `t`, the ordered pair `(x, y)` is an element of `P`. This theorem is essentially asserting a characterization for when a Cartesian product of two sets is a subset of a third set, in terms of individual elements of the original sets.
More concisely: For sets `s` of type `α`, `t` of type `β`, and `P` of type `(α × β)`, `s × t ⊆ P` if and only if for all `x ∈ s` and `y ∈ t`, `(x, y) ∈ P`.
|
Set.fst_image_prod
theorem Set.fst_image_prod :
∀ {α : Type u_1} {β : Type u_2} (s : Set β) {t : Set α}, t.Nonempty → Prod.fst '' s ×ˢ t = s
The theorem `Set.fst_image_prod` states that for any two types `α` and `β`, and any set `s` of type `β` and a nonempty set `t` of type `α`, the image of the first projection function `Prod.fst` applied to the Cartesian product of `s` and `t` is equal to `s`. In more mathematical terms, for every element in set `s`, there exists a pair in the Cartesian product of `s` and `t` such that the first element of the pair belongs to `s`. This element is the image of the pair under the first projection function. Thus, the set of all the first elements of the pairs in the Cartesian product is equal to `s`.
More concisely: The first projection of the Cartesian product of two sets maps each element of one set to an element of that set itself.
|
Mathlib.Data.Set.Prod._auxLemma.17
theorem Mathlib.Data.Set.Prod._auxLemma.17 : ∀ {α : Type u} (x : α) (a b : Set α), (x ∈ a ∪ b) = (x ∈ a ∨ x ∈ b) := by
sorry
The theorem `Mathlib.Data.Set.Prod._auxLemma.17` asserts that for any type `α`, given an element `x` of type `α` and two sets `a` and `b` of type `α`, the statement "x is an element of the union of sets a and b" is equivalent to the statement "x is an element of set a or x is an element of set b". In other words, it establishes that the union operation in set theory corresponds to the logical disjunction operation in propositional logic.
More concisely: For any type α and sets A and B of type α, the element x ∈ α belongs to the union A ∪ B if and only if x ∈ A or x ∈ B.
|
Set.mk_preimage_prod_right
theorem Set.mk_preimage_prod_right :
∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {a : α}, a ∈ s → Prod.mk a ⁻¹' s ×ˢ t = t
This theorem states that for any given types `α` and `β`, a set `s` of type `α`, a set `t` of type `β`, and an element `a` of type `α`, if `a` is an element of `s`, then the preimage of the cartesian product of `s` and `t` under the function `Prod.mk a` (which pairs `a` with elements of `β`) is equal to `t`. In terms of set theory, if we have an element from one set, then the set of all pairs consisting of this element and an element from another set is equivalent to the second set.
More concisely: For any sets `α`, `β`, a set `s` of type `α`, a set `t` of type `β`, and an element `a` of type `α` in `s`, the preimage of the cartesian product `s × t` under the function `Prod.mk a` is equal to `t`. In symbols: `{x : β | ∃ s. (a ∈ s) ∧ (x, a) ∈ s × t} = t`.
|
Set.Nonempty.snd
theorem Set.Nonempty.snd : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, (s ×ˢ t).Nonempty → t.Nonempty := by
sorry
This theorem states that for any two types `α` and `β`, and any two sets `s` of type `α` and `t` of type `β`, if the Cartesian product of `s` and `t` (denoted as `s ×ˢ t`) is nonempty, then the set `t` must also be nonempty. In mathematical terms, if there exists at least one ordered pair `(x, y)` such that `x` is in `s` and `y` is in `t`, then there must exist at least one element in `t`.
More concisely: If a cartesian product of non-empty sets is nonempty, then each of the sets is nonempty.
|
Set.prod_eq_empty_iff
theorem Set.prod_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β}, s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
The theorem `Set.prod_eq_empty_iff` states that for any types `α` and `β`, and any sets `s` of type `α` and `t` of type `β`, the Cartesian product of `s` and `t` is empty if and only if either `s` or `t` is empty. In other words, a Cartesian product of two sets is empty if at least one of those sets is empty.
More concisely: The Cartesian product of two sets is empty if and only if one of the sets is empty.
|
Set.preimage_prod_map_prod
theorem Set.preimage_prod_map_prod :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (s : Set β) (t : Set δ),
Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t)
The theorem `Set.preimage_prod_map_prod` states that for any types `α`, `β`, `γ`, and `δ`, and any functions `f : α → β` and `g : γ → δ`, and for any sets `s` of type `β` and `t` of type `δ`, the preimage of the product of `s` and `t` under the product map created by `f` and `g` is equal to the product of the preimages of `s` and `t` under `f` and `g`, respectively. In other words, mapping a pair of elements and then taking their preimages is the same as taking the preimages of the elements first and then forming a pair. This theorem is important in the theory of functions and sets as it describes a fundamental property of preimages under functions.
More concisely: For any functions `f : α → β` and `g : γ → δ`, and sets `s �venue β` and `t �venue δ`, the preimage of `s × t` under the product map of `f` and `g` equals the product of the preimages of `s` under `f` and `t` under `g`.
|
Set.univ_pi_singleton
theorem Set.univ_pi_singleton :
∀ {ι : Type u_1} {α : ι → Type u_2} (f : (i : ι) → α i), (Set.univ.pi fun i => {f i}) = {f}
The theorem `Set.univ_pi_singleton` states that for any type of indices `ι` and any family of types `α` indexed by `ι`, for any function `f` from `ι` to `α`, the set of all dependent functions `g : Πa, α a` such that `g a` belongs to the singleton set `{f a}` for all `a` in the universal set (which contains all indices) is precisely the singleton set `{f}`. In other words, the only function that maps each index to its corresponding value in `f` is `f` itself.
More concisely: For any type of indices ι and any family of types α indexed by ι, the dependent function Πa, α a that maps each index a to the unique element in {fa} is exactly the function f.
|
Set.image_swap_prod
theorem Set.image_swap_prod : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) (t : Set β), Prod.swap '' s ×ˢ t = t ×ˢ s
This theorem states that for any sets `s` of type `α` and `t` of type `β`, the image of the cartesian product `s ×ˢ t` under the `Prod.swap` operation equals the cartesian product `t ×ˢ s`. Here, `Prod.swap` is an operation that swaps the elements in a pair, and `''` represents the image of a set under a function. The `×ˢ` operation represents the cartesian product of two sets. So in essence, this theorem states that swapping the elements in each pair of the cartesian product of two sets results in the cartesian product of the sets in reverse order.
More concisely: For any sets `α` and `β`, the image of `s ×ˢ t` under `Prod.swap` equals `t ×ˢ s`, where `s ×ˢ t` is the cartesian product of `s` and `t`.
|
Set.prod_inter_prod
theorem Set.prod_inter_prod :
∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β}, s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ = (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂) := by
sorry
This theorem states that for any types `α` and `β`, and any sets `s₁`, `s₂` of type `α` and `t₁`, `t₂` of type `β`, the intersection of the Cartesian product of `s₁` and `t₁` with the Cartesian product of `s₂` and `t₂` is equal to the Cartesian product of the intersection of `s₁` and `s₂` with the intersection of `t₁` and `t₂`. In mathematical terms, this can be written as $(s₁ \times t₁) \cap (s₂ \times t₂) = (s₁ \cap s₂) \times (t₁ \cap t₂)$.
More concisely: The intersection of two Cartesian products of sets is equal to the Cartesian product of their intersections: $(s\_1 \times t\_1) \cap (s\_2 \times t\_2) = (s\_1 \cap s\_2) \times (t\_1 \cap t\_2)$.
|
Set.prod_subset_prod_iff
theorem Set.prod_subset_prod_iff :
∀ {α : Type u_1} {β : Type u_2} {s s₁ : Set α} {t t₁ : Set β},
s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
The theorem `Set.prod_subset_prod_iff` states that for any types `α` and `β`, and any sets `s` and `s₁` of type `α`, and `t` and `t₁` of type `β`, the cartesian product of `s` and `t` is a subset of the cartesian product of `s₁` and `t₁` if and only if either `s` is a subset of `s₁` and `t` is a subset of `t₁`, or `s` is an empty set, or `t` is an empty set. In other words, a cartesian product of two sets is contained within another cartesian product of two sets if either both sets are subsets of the corresponding sets in the second product, or one of the sets in the first product is empty.
More concisely: For sets `s` of type `α` and `t` of type `β`, `Set.prod s t ⊆ Set.prod s₁ t₁` if and only if `s ⊆ s₁` and `t ⊆ t₁`, or `s = ∅` or `t = ∅`.
|