-
Notifications
You must be signed in to change notification settings - Fork 299
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] - chore(topology/separation): Extract set
product lemma
#14958
Conversation
@@ -617,7 +617,8 @@ begin | |||
∑ i in s.preimage sum.inr (sum.inr_injective.inj_on _), (λ x, g x • v x) (sum.inr i) = 0, | |||
{ rw [finset.sum_preimage', finset.sum_preimage', ← finset.sum_union, ← finset.filter_or], | |||
{ simpa only [← mem_union, range_inl_union_range_inr, mem_univ, finset.filter_true] }, | |||
{ exact finset.disjoint_filter.2 (λ x hx, disjoint_left.1 is_compl_range_inl_range_inr.1) } }, | |||
{ exact finset.disjoint_filter.2 | |||
(λ x _ hx, disjoint_left.1 is_compl_range_inl_range_inr.1 hx) } }, |
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 did this proof become longer?
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.
It's because I changed disjoint_left
to have a semi-implicit argument on the RHS. It seems to be the right choice everywhere but here.
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.
Please mention this in the commit message. Otherwise LGTM.
bors d+
lemma _root_.disjoint.inter_eq : disjoint s t → s ∩ t = ∅ := disjoint.eq_bot | ||
|
||
lemma disjoint_left : disjoint s t ↔ ∀ ⦃a⦄, a ∈ s → a ∉ t := forall_congr $ λ _, not_and | ||
lemma disjoint_right : disjoint s t ↔ ∀ ⦃a⦄, a ∈ t → a ∉ s := by rw [disjoint.comm, disjoint_left] |
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.
Idea for the future: some lemmas in this file have disjoint
in the name and s ∩ t = ∅
in the statement. It would be nice to fix this.
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.
This is what #14950 does 😄 (for some of them).
@@ -617,7 +617,8 @@ begin | |||
∑ i in s.preimage sum.inr (sum.inr_injective.inj_on _), (λ x, g x • v x) (sum.inr i) = 0, | |||
{ rw [finset.sum_preimage', finset.sum_preimage', ← finset.sum_union, ← finset.filter_or], | |||
{ simpa only [← mem_union, range_inl_union_range_inr, mem_univ, finset.filter_true] }, | |||
{ exact finset.disjoint_filter.2 (λ x hx, disjoint_left.1 is_compl_range_inl_range_inr.1) } }, | |||
{ exact finset.disjoint_filter.2 | |||
(λ x _ hx, disjoint_left.1 is_compl_range_inl_range_inr.1 hx) } }, |
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.
Please mention this in the commit message. Otherwise LGTM.
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks both! bors merge |
Move `prod_subset_compl_diagonal_iff_disjoint` to `data.set.prod`, where it belongs. Delete `diagonal_eq_range_diagonal_map` because it duplicates `set.diagonal_eq_range`. Move `set.disjoint_left`/`set.disjoint_right` to `data.set.basic` to avoid an import cycle. Make variable semi-implicit in the RHS of `disjoint_left` and `disjoint_right`.
Pull request successfully merged into master. Build succeeded: |
set
product lemmaset
product lemma
Move `prod_subset_compl_diagonal_iff_disjoint` to `data.set.prod`, where it belongs. Delete `diagonal_eq_range_diagonal_map` because it duplicates `set.diagonal_eq_range`. Move `set.disjoint_left`/`set.disjoint_right` to `data.set.basic` to avoid an import cycle. Make variable semi-implicit in the RHS of `disjoint_left` and `disjoint_right`.
Move
prod_subset_compl_diagonal_iff_disjoint
todata.set.prod
, where it belongs. Deletediagonal_eq_range_diagonal_map
because it duplicatesset.diagonal_eq_range
. Moveset.disjoint_left
/set.disjoint_right
todata.set.basic
to avoid an import cycle.Make variable semi-implicit in the RHS of
disjoint_left
anddisjoint_right
.