-
Notifications
You must be signed in to change notification settings - Fork 247
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat: Product of injective functions on sets #12656
Conversation
YaelDillies
commented
May 4, 2024
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maintainer merge
variable {α₁ α₂ β₁ β₂ : Type*} {s₁ : Set α₁} {s₂ : Set α₂} {t₁ : Set β₁} {t₂ : Set β₂} | ||
{f₁ : α₁ → β₁} {f₂ : α₂ → β₂} {g₁ : β₁ → α₁} {g₂ : β₂ → α₂} | ||
|
||
lemma InjOn.prodMap (h₁ : s₁.InjOn f₁) (h₂ : s₂.InjOn f₂) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I find dot notation for InjOn doesn't really read well, but won't block on it
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why not use Prod.map
in the statements?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
because it gets simplified to its definition as Prod_map
(not a typo!!) is a simp lemma
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
@@ -1041,6 +1041,14 @@ theorem BijOn.image_eq (h : BijOn f s t) : f '' s = t := | |||
h.surjOn.image_eq_of_mapsTo h.mapsTo | |||
#align set.bij_on.image_eq Set.BijOn.image_eq | |||
|
|||
lemma BijOn.forall {p : β → Prop} (hf : BijOn f s t) : (∀ b ∈ t, p b) ↔ ∀ a ∈ s, p (f a) where | |||
mp h a ha := h _ $ hf.mapsTo ha | |||
mpr h b hb := by obtain ⟨a, ha, rfl⟩ := hf.surjOn hb; exact h _ ha |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Alternative proof: by rw [← hf.image_eq, forall_mem_image]
Thanks! 🎉 |
Pull request successfully merged into master. Build succeeded: |