From 4e68c730e208047ed4a303895fdaed665a892438 Mon Sep 17 00:00:00 2001 From: Xavier Roblot Date: Fri, 10 May 2024 15:40:43 +0000 Subject: [PATCH] feat: add `Equiv.prodSubtypeFstEquivSubtypeProd` (#12802) See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/A.20basic.20equivalence/near/437968727) Co-authored-by: Xavier Roblot <46200072+xroblot@users.noreply.github.com> --- Mathlib/Logic/Equiv/Basic.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/Logic/Equiv/Basic.lean b/Mathlib/Logic/Equiv/Basic.lean index fdeffe6781920a..9c06c142682d58 100644 --- a/Mathlib/Logic/Equiv/Basic.lean +++ b/Mathlib/Logic/Equiv/Basic.lean @@ -1380,6 +1380,14 @@ def subtypeProdEquivProd {p : α → Prop} {q : β → Prop} : right_inv := fun ⟨⟨_, _⟩, ⟨_, _⟩⟩ => rfl #align equiv.subtype_prod_equiv_prod Equiv.subtypeProdEquivProd +/-- 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. -/ +def prodSubtypeFstEquivSubtypeProd {p : α → Prop} : {s : α × β // p s.1} ≃ {a // p a} × β where + toFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩ + invFun x := ⟨⟨x.1.1, x.2⟩, x.1.2⟩ + left_inv _ := rfl + right_inv _ := rfl + /-- A subtype of a `Prod` is equivalent to a sigma type whose fibers are subtypes. -/ def subtypeProdEquivSigmaSubtype (p : α → β → Prop) : { x : α × β // p x.1 x.2 } ≃ Σa, { b : β // p a b } where