Equivalence between product types #
In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean
,
focussing on product types.
Main definitions #
Equiv.prodCongr ea eb : α₁ × β₁ ≃ α₂ × β₂
: combine two equivalencesea : α₁ ≃ α₂
andeb : β₁ ≃ β₂
usingProd.map
.
Tags #
equivalence, congruence, bijective map
Any Unique
type is a left identity for type sigma up to equivalence. Compare with uniqueProd
which is non-dependent.
Equations
Instances For
PEmpty
type is a right absorbing element for type product up to an equivalence.
Equations
Instances For
PEmpty
type is a left absorbing element for type product up to an equivalence.
Equations
Instances For
A variation on Equiv.prodCongr
where the equivalence in the second component can depend
on the first component. A typical example is a shear mapping, explaining the name of this
declaration.
Equations
Instances For
prodExtendRight a e
extends e : Perm β
to Perm (α × β)
by sending (a, b)
to
(a, e b)
and keeping the other (a', b)
fixed.
Equations
Instances For
The type of dependent functions on a sum type ι ⊕ ι'
is equivalent to the type of pairs of
functions on ι
and on ι'
. This is a dependent version of Equiv.sumArrowEquivProdArrow
.
Equations
Instances For
The equivalence between a product of two dependent functions types and a single dependent
function type. Basically a symmetric version of Equiv.sumPiEquivProdPi
.
Equations
Instances For
A subtype of a Prod
that depends only on the first component is equivalent to the
corresponding subtype of the first type times the second type.
Equations
Instances For
The type ∀ (i : α), β i
can be split as a product by separating the indices in α
depending on whether they satisfy a predicate p
or not.
Equations
Instances For
If α
is a subsingleton, then it is equivalent to α × α
.