English
A product of subtypes defined componentwise is equivalent to the product of subtypes: Subtype (p) × Subtype (q) ≃ Subtype (p) × Subtype (q).
Русский
Произведение подтипов, заданное покомпонентно, эквивалентно произведению подтипов: Subtype p × Subtype q ≃ Subtype p × Subtype q.
LaTeX
$$$\text{Equiv} \big(\text{Subtype } (p) \times \text{Subtype } (q)\big) \simeq \text{Subtype }(p) \times \text{Subtype }(q).$$$
Lean4
/-- A subtype of a product defined by componentwise conditions
is equivalent to a product of subtypes. -/
def subtypeProdEquivProd {α β} {p : α → Prop} {q : β → Prop} :
{ c : α × β // p c.1 ∧ q c.2 } ≃ { a // p a } × { b // q b }
where
toFun := fun x => ⟨⟨x.1.1, x.2.1⟩, ⟨x.1.2, x.2.2⟩⟩
invFun := fun x => ⟨⟨x.1.1, x.2.1⟩, ⟨x.1.2, x.2.2⟩⟩
