Equiv.Perm.subtypeCongr.right_apply
theorem Equiv.Perm.subtypeCongr.right_apply :
∀ {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a })
(en : Equiv.Perm { a // ¬p a }) {a : ε} (h : ¬p a), (ep.subtypeCongr en) a = ↑(en ⟨a, h⟩)
The theorem `Equiv.Perm.subtypeCongr.right_apply` states that for any type `ε`, predicate `p` on `ε`, a permutation `ep` on elements satisfying `p`, a permutation `en` on elements not satisfying `p`, and an element `a` of `ε` that does not satisfy `p`, applying the permutation constructed by `Equiv.Perm.subtypeCongr` using `ep` and `en` to `a` results in the same value as applying `en` to `a` (cast to the subtype of elements not satisfying `p`). This means that inside the subset where `p` is not satisfied, the combined permutation acts exactly as `en`.
More concisely: For any type `ε`, predicate `p` on `ε`, permutations `ep` on elements of `p` and `en` on elements of `¬p`, and element `a` not in `p`, `Equiv.Perm.subtypeCongr.right_apply ep en a = en a`.
|
Equiv.symm_swap
theorem Equiv.symm_swap : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), (Equiv.swap a b).symm = Equiv.swap a b
The theorem `Equiv.symm_swap` states that for any type `α` that has decidable equality, and for any two elements `a` and `b` of type `α`, the inverse of the permutation that swaps `a` and `b` (denoted as `(Equiv.swap a b).symm`) is actually the same as the original permutation that swaps `a` and `b` (denoted as `Equiv.swap a b`). In essence, this theorem confirms that swapping `a` and `b` twice will return to the original arrangement, regardless of the type `α` as long as equality is decidable for that type. This can be seen as a generalization of the fact that the inverse of a swap operation in basic combinatorics is the swap operation itself.
More concisely: For any type `α` with decidable equality, the inverse of swapping elements `a` and `b` is equivalent to swapping them back, i.e., `(Equiv.swap a b).symm = Equiv.swap a b`.
|
Equiv.swap_apply_right
theorem Equiv.swap_apply_right : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), (Equiv.swap a b) b = a
The theorem `Equiv.swap_apply_right` states that for any type `α` that has decidable equality, given any two elements `a` and `b` of type `α`, applying the "swap" permutation (which is defined such that it swaps `a` and `b` and leaves other values unchanged) to `b` results in `a`. In other words, if we swap `a` and `b` and then look at the position of `b`, we will find `a` there.
More concisely: For any type `α` with decidable equality and any `a, b : α`, swapping `a` and `b` yields `b` becoming equal to `a`.
|
Equiv.swap_apply_def
theorem Equiv.swap_apply_def :
∀ {α : Sort u_1} [inst : DecidableEq α] (a b x : α),
(Equiv.swap a b) x = if x = a then b else if x = b then a else x
The theorem `Equiv.swap_apply_def` states that for any type `α` with decidable equality and any elements `a`, `b`, and `x` of type `α`, the result of applying the permutation that swaps `a` and `b` to `x` (denoted as `(Equiv.swap a b) x`), is `b` if `x` equals `a`, `a` if `x` equals `b`, and `x` otherwise. In other words, the permutation only affects `x` if it is equal to `a` or `b`.
More concisely: For any type with decidable equality and elements `a`, `b`, and `x`, `Equiv.swap a b x = a if x = b else b if x = a else x`.
|
Equiv.isEmpty
theorem Equiv.isEmpty : ∀ {α : Sort u_1} {β : Sort u_2}, α ≃ β → ∀ [inst : IsEmpty β], IsEmpty α
The theorem `Equiv.isEmpty` states that for any sorts `α` and `β`, if `α` is equivalent to `β` and `β` is empty (as indicated by the instance `IsEmpty β`), then `α` is also empty (the result is `IsEmpty α`). Essentially, this theorem links the emptiness of two equivalent sorts: the emptiness of one ensures the emptiness of the other.
More concisely: If `α` is equivalent to an empty sort `β`, then `α` is also empty.
|
Equiv.swap_self
theorem Equiv.swap_self : ∀ {α : Sort u_1} [inst : DecidableEq α] (a : α), Equiv.swap a a = Equiv.refl α
This theorem, `Equiv.swap_self`, asserts that for any type `α` with decidable equality and for any element `a` of type `α`, the permutation function that swaps `a` with itself is equivalent to the identity function on `α`. In other words, swapping an element with itself leaves all elements in place, thus producing the identity permutation.
More concisely: For any type `α` with decidable equality and any element `a` of type `α`, the identity function and the function that swaps `a` with itself are equal as permutations on `α`.
|
Mathlib.Logic.Equiv.Basic._auxLemma.2
theorem Mathlib.Logic.Equiv.Basic._auxLemma.2 : (¬False) = True
This theorem, `Mathlib.Logic.Equiv.Basic._auxLemma.2`, states that the negation of `False` is `True`. In other words, it's expressing the basic logic principle that if something is not false, then it must be true.
More concisely: The theorem asserts that the negation of False is True. In mathematical notation, ¬False = True.
|
Equiv.piCongrLeft'_symm
theorem Equiv.piCongrLeft'_symm :
∀ {α : Sort u_2} {β : Sort u_3} (P : Sort u_1) (e : α ≃ β),
(Equiv.piCongrLeft' (fun x => P) e).symm = Equiv.piCongrLeft' (fun a => P) e.symm
This theorem states that for any types `α` and `β`, and any type family `P`, the inverse of the equivalence that transports dependent functions through an equivalence of the base space, given by `Equiv.piCongrLeft'`, is equal to the direct equivalence that transports dependent functions through the inverse of the original equivalence. This theorem essentially asserts the symmetry property of the transportation of dependent functions through equivalent base spaces.
More concisely: For any type families `P` and types `α` and `β`, `Equiv.piCongrLeft' (Equiv.symm _) (Equiv.piCongrLeft' f g) = Equiv.piCongrRight' g (Equiv.symm _) f`, where `f : α ≃ β` is an equivalence and `g : P α ≃ P β`.
|
Equiv.Perm.extendDomain_apply_image
theorem Equiv.Perm.extendDomain_apply_image :
∀ {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
(a : α'), (e.extendDomain f) ↑(f a) = ↑(f (e a))
The theorem `Equiv.Perm.extendDomain_apply_image` states that for all types `α'` and `β'`, given a permutation `e` of `α'`, a decidable predicate `p` on `β'`, and a bijective function `f` from `α'` to the subtype of `β'` satisfying `p`, then for any element `a` of `α'`, the extended permutation applied to the image of `a` under `f` is equal to the image of the image of `a` under `e` through `f`. In other words, this theorem is about the interaction between the projection of a permutation and the extension of a permutation with the same bijective function.
More concisely: Given a permutation `e` of type `α'`, a bijective function `f` from `α'` to a subtype of `β'` satisfying a decidable predicate `p`, and an element `a` of `α'`, the extended permutation applied to `f(a)` is equal to `f(e(a))`.
|
Equiv.swap_apply_left
theorem Equiv.swap_apply_left : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), (Equiv.swap a b) a = b
The theorem `Equiv.swap_apply_left` states that for any type `α` with decidable equality and any two elements `a` and `b` of `α`, applying the permutation that swaps `a` and `b` to `a` results in `b`. In other words, when we have a permutation that exchanges `a` and `b` and leaves other values unchanged, applying this permutation to `a` will give us `b`.
More concisely: For any type `α` with decidable equality and any `a, b : α`, swapping `a` and `b` yields `b` when `a` is permuted.
|
Equiv.piCongrLeft'_symm_apply
theorem Equiv.piCongrLeft'_symm_apply :
∀ {α : Sort u_2} {β : Sort u_3} (P : α → Sort u_1) (e : α ≃ β) (f : (b : β) → P (e.symm b)) (x : α),
(Equiv.piCongrLeft' P e).symm f x = ⋯ ▸ f (e x)
This theorem states that for any sorts `α` and `β`, a function `P : α → Sort u_1`, an equivalence `e : α ≃ β`, a dependent function `f : (b : β) → P (e.symm b)`, and an element `x : α`, the application of the inverse of the dependent type transport through the equivalence `e` on `f` at `x` is equal to the application of `f` at the image of `x` under `e`, up to a proof `⋯` that `e.symm (e x) = x`. Note that a direct equality `f (e x)` doesn't type check, hence the need for this theorem which assures the equality after a substitution along `e.symm (e x) = x`.
More concisely: For any equivalence `e : α ≃ β`, function `P : α → Sort u_1`, dependent function `f : β → P (e _)`, and element `x : α`, the application of `f` at the image of `x` under `e` is equal to the application of the transport of `f` along `e` at `x`, up to the reflexivity of `e`.
|
Equiv.apply_swap_eq_self
theorem Equiv.apply_swap_eq_self :
∀ {α : Sort u_2} [inst : DecidableEq α] {β : Sort u_1} {v : α → β} {i j : α},
v i = v j → ∀ (k : α), v ((Equiv.swap i j) k) = v k
The theorem `Equiv.apply_swap_eq_self` states that for any types `α` and `β`, and given a function `v` mapping from `α` to `β`, and any elements `i` and `j` in `α`, if `v` applied to `i` equals `v` applied to `j`, then for all elements `k` in `α`, applying `v` to the result of swapping `i` and `j` in `k` using the swap equivalence (`Equiv.swap i j k`) yields the same result as simply applying `v` to `k`. In other words, the function `v` is invariant to swapping `i` and `j` in its argument.
More concisely: For all types α and β, and functions v : α -> β, if v i = v j, then for all k in α, v (Equiv.swap i j k) = v k.
|
Equiv.isEmpty_congr
theorem Equiv.isEmpty_congr : ∀ {α : Sort u_1} {β : Sort u_2}, α ≃ β → (IsEmpty α ↔ IsEmpty β)
This theorem states that if there is an equivalence between two types `α` and `β`, then `α` is empty if and only if `β` is empty. In other words, the emptiness property is preserved under equivalence between the types. This theorem is applicable to types `α` and `β` located in arbitrary sorts.
More concisely: If `α` is equivalent to `β`, then `α` is empty if and only if `β` is empty.
|
Equiv.piCongrLeft_apply
theorem Equiv.piCongrLeft_apply :
∀ {β : Sort u_1} {α : Sort u_2} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (b : β),
(Equiv.piCongrLeft P e) f b = ⋯ ▸ f (e.symm b)
The theorem `Equiv.piCongrLeft_apply` describes how to apply a dependent function that has been transported through a base equivalence using `Equiv.piCongrLeft`. For any sorts `α` and `β`, an equivalence `e` between `α` and `β`, a dependent function `f: (a: α) → P(e a)`, and a value `b` of type `β`, applying the function `f` after transporting it through the equivalence `e` to the value `b` equals applying `f` to the preimage of `b` under `e`, after substituting `e (e.symm b) = b`. Please note that a naïve equation might not type-check because the left-hand side would have type `P b` while the right-hand side would have type `P (e (e.symm b))`, hence the explicit substitution.
More concisely: For any equivalence `e` between types `α` and `β`, dependent function `f : α → P(e x)`, and value `b` of type `β`, applying `f` to the preimage of `b` under `e` and substituting `e (e⁻¹ b) = b` is equal to transporting and applying `f`.
|
Equiv.Perm.subtypeCongr.left_apply
theorem Equiv.Perm.subtypeCongr.left_apply :
∀ {ε : Type u_1} {p : ε → Prop} [inst : DecidablePred p] (ep : Equiv.Perm { a // p a })
(en : Equiv.Perm { a // ¬p a }) {a : ε} (h : p a), (ep.subtypeCongr en) a = ↑(ep ⟨a, h⟩)
The theorem `Equiv.Perm.subtypeCongr.left_apply` states that for any type `ε`, and any predicate `p` on `ε` that is decidable, given a permutation `ep` on the subtype of elements of `ε` that satisfy `p` and a permutation `en` on the subtype of elements of `ε` that do not satisfy `p`, for any element `a` of `ε` that satisfies `p`, applying the combined permutation `Equiv.Perm.subtypeCongr ep en` to `a` is the same as applying the permutation `ep` to `a` (thought of as an element of the subtype `{ a // p a }`), and then taking the underlying element of `ε`. In other words, for elements that satisfy the predicate, the combined permutation behaves just like the permutation on the satisfying subtype.
More concisely: For any type `ε`, decidable predicate `p` on `ε`, permutations `ep` on the subtype of elements of `ε` satisfying `p` and `en` on the complement subtype, and element `a` of `ε` satisfying `p`, `Equiv.Perm.subtypeCongr ep en a` equals `ep a`.
|
Equiv.swap_apply_of_ne_of_ne
theorem Equiv.swap_apply_of_ne_of_ne :
∀ {α : Sort u_1} [inst : DecidableEq α] {a b x : α}, x ≠ a → x ≠ b → (Equiv.swap a b) x = x
The theorem `Equiv.swap_apply_of_ne_of_ne` states that for any type `α` that has decidable equality (expressed by `DecidableEq α`), and for any three elements `a`, `b`, and `x` of that type, if `x` is not equal to `a` and `x` is not equal to `b`, then applying the swap operation `Equiv.swap a b` to `x` leaves `x` unchanged. In other words, the function `Equiv.swap a b` acts as the identity on elements distinct from `a` and `b`. This swap operation, `Equiv.swap a b`, is a permutation that swaps the positions of `a` and `b` and leaves all other elements as they are.
More concisely: For any type `α` with decidable equality and distinct elements `a`, `b`, and `x` of `α`, `Equiv.swap a b x = x`.
|
Equiv.swap_swap
theorem Equiv.swap_swap :
∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), (Equiv.swap a b).trans (Equiv.swap a b) = Equiv.refl α := by
sorry
The theorem `Equiv.swap_swap` states that for any type `α` with decidable equality and any two elements `a` and `b` of `α`, the composition (or "trans", short for "transitive") of the permutation that swaps `a` and `b` with itself is equivalent to the identity permutation on `α`. In other words, if we swap `a` and `b` twice, we get back to the original arrangement, which is the same as doing nothing (the identity operation).
More concisely: For any type `α` with decidable equality and any two elements `a` and `b` in `α`, the swap permutation of `a` and `b` is idempotent.
|
Equiv.subtypeEquiv.proof_1
theorem Equiv.subtypeEquiv.proof_1 :
∀ {α : Sort u_2} {β : Sort u_1} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
(∀ (a : α), p a ↔ q (e a)) → ∀ (a : { a // p a }), q (e ↑a)
This theorem states that for any two types `α` and `β` and two properties `p` on `α` and `q` on `β`, given an equivalence `e` between `α` and `β`, if for all `a` of type `α`, `p a` is equivalent to `q (e a)`, then for all `a` that satisfy `p`, `q (e ↑a)` holds. In other words, if a property `p` holds for elements in type `α` and this property is equivalent to another property `q` holding for the corresponding elements in type `β` under some equivalence, then the property `q` holds for all such equivalent elements.
More concisely: If `e` is an equivalence between types `α` and `β`, and `p` on `α` is equivalent to `q` on `β` via `e`, then for all `a` of type `α` with property `p`, `q` holds for their equivalence classes `[a]` under `e`.
|
Equiv.swap_comm
theorem Equiv.swap_comm : ∀ {α : Sort u_1} [inst : DecidableEq α] (a b : α), Equiv.swap a b = Equiv.swap b a
The theorem `Equiv.swap_comm` states that for any type `α` that has decidable equality, the permutation that swaps `a` and `b` is the same as the permutation that swaps `b` and `a`. In other words, for any elements `a` and `b` of a type `α`, swapping `a` and `b` is commutative. This means that the order of the elements does not affect the result of the swap operation, i.e., `Equiv.swap a b` equals `Equiv.swap b a`, regardless of what the specific elements `a` and `b` are.
More concisely: For any type `α` with decidable equality, the swap operation between elements `a` and `b` is commutative, i.e., `Equiv.swap a b` equals `Equiv.swap b a`.
|
Equiv.piCongrLeft'_symm_apply_apply
theorem Equiv.piCongrLeft'_symm_apply_apply :
∀ {α : Sort u_2} {β : Sort u_3} (P : α → Sort u_1) (e : α ≃ β) (g : (b : β) → P (e.symm b)) (b : β),
(Equiv.piCongrLeft' P e).symm g (e.symm b) = g b
This theorem states that for any types `α` and `β`, a dependent function `P : α → Sort u_1` and an equivalence `e : α ≃ β`, and a function `g : (b : β) → P (e.symm b)`, applying the inverse of the transformation function `Equiv.piCongrLeft'` (which transforms dependent functions through an equivalence of the base space) to `g` at `e.symm b` is equal to `g b`. In other words, it shows that when `a` is of the form `e.symm b`, we can simply use `g b` instead of `g (e (e.symm b))`, solving a type mismatch issue.
More concisely: For any equivalence `e : α ≃ β`, dependent functions `P : α → Sort u_1` and `g : β → Sort u_1`, and `b : β`, we have `Equiv.piCongrLeft' g e.symm b = g b`.
|
Equiv.Perm.extendDomain_apply_not_subtype
theorem Equiv.Perm.extendDomain_apply_not_subtype :
∀ {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
{b : β'}, ¬p b → (e.extendDomain f) b = b
The theorem `Equiv.Perm.extendDomain_apply_not_subtype` states that for any types `α'` and `β'`, any permutation `e` on `α'`, any decidable predicate `p` on `β'`, and any equivalence `f` between `α'` and the subtype of `β'` satisfying `p`, if an element `b` from `β'` does not satisfy the predicate `p`, then applying the extended permutation `Equiv.Perm.extendDomain e f` to `b` leaves `b` unchanged. In other words, the extended permutation does not alter elements which do not satisfy the predicate.
More concisely: For any equivalence `f` between types `α'` and a subtype of `β'` satisfying a decidable predicate `p` on `β'`, and any permutation `e` on `α'`, if an element `b` from `β'` does not satisfy `p`, then `Equiv.Perm.extendDomain e f b = b`.
|
Equiv.subtypeEquiv.proof_2
theorem Equiv.subtypeEquiv.proof_2 :
∀ {α : Sort u_1} {β : Sort u_2} {p : α → Prop} {q : β → Prop} (e : α ≃ β),
(∀ (a : α), p a ↔ q (e a)) → ∀ (b : { b // q b }), p (e.symm ↑b)
This theorem states that for any types `α` and `β`, and predicates `p` and `q` on `α` and `β` respectively, given an equivalence `e` from `α` to `β`, if for all `a` in `α`, `p a` if and only if `q (e a)`, then for every `b` in the subtype `{ b // q b }` (that is, for every `b` that satisfies the predicate `q`), `p (e.symm ↑b)` holds true. This essentially shows that a property `p` is preserved under the inverse of the equivalence `e` when applied to the elements of the subtype defined by `q`.
More concisely: If `e: α ↔ β` is an equivalence and `p: α → Prop` and `q: β → Prop` are predicates such that `p a ↔ q (e a)` for all `a: α`, then for every `b: {b // q b}`, `p (e.symm ↑b)` holds.
|
Equiv.Perm.extendDomain_apply_subtype
theorem Equiv.Perm.extendDomain_apply_subtype :
∀ {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
{b : β'} (h : p b), (e.extendDomain f) b = ↑(f (e (f.symm ⟨b, h⟩)))
The theorem `Equiv.Perm.extendDomain_apply_subtype` states that for any types `α'` and `β'`, a permutation `e` on `α'`, a decidable predicate `p` on `β'`, and a bijection `f` between `α'` and the subtype of `β'` satisfying `p`, the result of extending the domain of the permutation `e` using `f` and then applying it to any element `b` of `β'` that satisfies the predicate `p`, is equal to the result of applying `f` to the permutation `e` applied to the preimage of `{val := b, property := h}` under `f`.
In other words, the theorem describes how a permutation on a type `α'` can be extended to a permutation on a type `β'` using a bijection between `α'` and a subtype of `β'`.
More concisely: Given a permutation on a type `α'`, a bijection to a subtype of `β'` satisfying a decidable predicate, and an element in the subtype, the permutation extended using the bijection and applied to the element is equal to applying the bijection to the permutation and then to the preimage under the bijection.
|
Equiv.piCongrLeft_apply_apply
theorem Equiv.piCongrLeft_apply_apply :
∀ {β : Sort u_1} {α : Sort u_2} (P : β → Sort w) (e : α ≃ β) (f : (a : α) → P (e a)) (a : α),
(Equiv.piCongrLeft P e) f (e a) = f a
The `Equiv.piCongrLeft_apply_apply` theorem states that for any types `α` and `β`, a function `P` from `β` to some `Sort w`, an equivalence `e` between `α` and `β`, and a dependent function `f` from `α` to `P (e a)`, applying the function given by the left congruence of `P` with respect to `e` to `f` and `e a`, is the same as directly applying `f` to `a`. This resolves a possible dimension mismatch issue where the left-hand side would have type `P b` while the right-hand side would have type `P (e (e.symm b))`.
More concisely: For any equivalence `e` between types `α` and `β`, function `P : β → Sort w`, and dependent function `f : α → P (e (x))`, the application of `f` to `x` is equal to the application of the left congruence of `P` with respect to `e` to `f`.
|
Equiv.piCongrLeft_apply_eq_cast
theorem Equiv.piCongrLeft_apply_eq_cast :
∀ {β : Sort u_2} {α : Sort u_1} {P : β → Sort v} {e : α ≃ β} (f : (a : α) → P (e a)) (b : β),
(Equiv.piCongrLeft P e) f b = cast ⋯ (f (e.symm b))
The theorem `Equiv.piCongrLeft_apply_eq_cast` states that for any sorts `α` and `β`, for any function `P` from `β` to another sort, for any equivalence `e` between `α` and `β`, and for any dependent function `f` from `α` to `P` of `e a`, if we apply the function `f` after the equivalence transformation `Equiv.piCongrLeft P e`, we obtain the same result as if we first applied the inverse of the equivalence `e` to `b` and then applied the function `f` (up to a proof-irrelevant cast). This cast acts as a "transport" across types, allowing us to treat the two sides as equal even though their type-level form might differ due to the application of equivalence `e`.
More concisely: For any equivalence between types `e : α ≈ β`, function `P : β → Sort`, dependent function `f : α → P`, and elements `a : α` and `b : β` related by `e`, `f (Equiv.piCongrLeft P e a) ≈ f (e.inverse b)`.
|
Equiv.subtypeEquivProp.proof_1
theorem Equiv.subtypeEquivProp.proof_1 :
∀ {α : Sort u_1} {p q : α → Prop}, p = q → ∀ (x : α), p x ↔ q ((Equiv.refl α) x)
This theorem states that for any type `α` and for any two properties `p` and `q` of `α`, if `p` is equal to `q`, then for any element `x` of `α`, `x` satisfies `p` if and only if `x` satisfies `q` under the identity equivalence (`Equiv.refl α`). Essentially, it shows that if two properties are the same, then their satisfaction by a particular element remains unchanged even when considered under the identity mapping.
More concisely: For any type `α` and properties `p` and `q` of `α`, if `p` equals `q`, then `x` has property `p` if and only if `x` has property `q` for all `x` in `α` (under the identity equivalence).
|