Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(order/filter/n_ary): Add lemma equating map₂ to map on the product #13490

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(order/filter/n_ary): Add lemma equating map₂ to map on the product #13490

wants to merge 7 commits into from

Conversation

berndlosert
Copy link
Collaborator

@berndlosert berndlosert commented Apr 17, 2022 •
edited by eric-wieser
Loading

Proof that map₂ is the image of the corresponding function α × β → γ.

Discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/filter.20map.E2.82.82.20as.20map

Open in Gitpod

eric-wieser
eric-wieser approved these changes Apr 19, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The arguments should be explicit, and probably in the same order as in the lemma statement - see my suggestions.

bors d+

src/order/filter/n_ary.lean Outdated Show resolved Hide resolved
src/order/filter/n_ary.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Apr 19, 2022

✌️ berndlosert can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the delegated The PR author may merge after reviewing final suggestions. label Apr 19, 2022
@berndlosert
Copy link
Collaborator Author

bors r+

bors bot pushed a commit that referenced this pull request Apr 19, 2022
@berndlosert
feat(order/filter/n_ary): Add lemma equating map₂ to map on the produ…
5dc8c1c 
…ct (#13490)

Proof that map₂ is the image of the corresponding function `α × β → γ`.

Discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/filter.20map.E2.82.82.20as.20map
@bors
Copy link

bors bot commented Apr 19, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/filter/n_ary): Add lemma equating map₂ to map on the product [Merged by Bors] - feat(order/filter/n_ary): Add lemma equating map₂ to map on the product Apr 19, 2022
@bors bors bot closed this Apr 19, 2022
@bors bors bot deleted the filter-map2-map branch April 19, 2022 15:52
Julian added a commit that referenced this pull request Apr 21, 2022
@Julian
Merge remote-tracking branch 'origin/master' into torsion-free-groups
eb3119e 
* origin/master: (394 commits)
  feat(data/set/[basic|prod]): make `×ˢ` bind more strongly, and define `mem.out` (#13422)
  feat(order/basic): Simple shortcut lemmas (#13421)
  chore(number_theory/dioph): Cleanup (#13403)
  feat(analysis/normed_space/exponential): ring homomorphisms are preserved by the exponential (#13402)
  feat(algebraic_geometry/projective_spectrum): degree zero part of a localized ring (#13398)
  feat(set_theory/cardinal): A set of cardinals is small iff it's bounded (#13373)
  feat(data/polynomial/{derivative, iterated_deriv}): reduce assumptions (#13368)
  feat(algebra/monoid_algebra/grading): Use the new graded_algebra API (#13360)
  feat(algebra/group/to_additive): let @[to_additive] mimic alias’s docstrings (#13330)
  feat(set_theory/cofinality): Basic fundamental sequences (#13326)
  feat(special_functions/pow): continuity of real to complex power (#13244)
  feat(group_theory/torsion): extension closedness, and torsion scalars in modules (#13172)
  feat(category_theory/path_category): canonical quotient of a path category (#13159)
  refactor(number_theory/padics/padic_norm): Switch nat and rat definitions (#12454)
  feat(analysis/normed): more lemmas about the sup norm on pi types and matrices (#13536)
  fix(category_theory/monoidal): improve hygiene in coherence tactic (#13507)
  feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465)
  chore(algebra/group/type_tags): missing simp lemmas (#13553)
  feat(measure_theory): allow measurability to prove ae_strongly_measurable (#13427)
  refactor(algebra/hom/group): generalize a few lemmas to `monoid_hom_class` (#13447)
  chore(data/list/cycle): Add basic `simp` lemmas + minor golfing (#13533)
  feat(algebra/hom/non_unital_alg): introduce notation for non-unital algebra homomorphisms (#13470)
  chore(algebra/group/defs): Declare `field_simps` attribute earlier (#13543)
  feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)
  refactor(analysis/calculus/cont_diff): reorder the file (#13468)
  move(set_theory/*): Organize in folders (#13530)
  chore(number_theory/zsqrtd/basic): simplify le_total proof (#13555)
  feat(group_theory/perm/basic): Iterating a permutation is the same as taking a power (#13554)
  feat(data/real/sqrt): `sqrt x < y ↔ x < y^2` (#13546)
  feat(algebra/hom/group and *): introduce `mul_hom M N` notation `M →ₙ* N` (#13526)
  feat(group_theory/schreier): Schreier's lemma in terms of `group.fg` and `group.rank` (#13361)
  feat(linear_algebra/trace): dual_tensor_hom is an equivalence + basis-free characterization of the trace (#10372)
  feat(order/filter/basic): allow functions between different types in lemmas about [co]map by a constant function (#13542)
  feat(data/finset/basic): simp `to_finset_eq_empty` (#13531)
  feat(topology/algebra/algebra): ℚ-scalar multiplication is continuous (#13458)
  chore(model_theory/encoding): Improve the encoding of terms  (#13532)
  feat(topology/separation): Finite sets in T2 spaces (#12845)
  feat(analysis/inner_product_space/gram_schmidt_ortho): Gram-Schmidt Orthogonalization and Orthonormalization (#12857)
  chore(algebra/big_operators/fin): golf finset.prod_range (#13535)
  chore(analysis/normed_space/star): make an argument explicit (#13523)
  feat(*): `op_op_op_comm` lemmas (#13528)
  chore(data/real/nnreal): add commuted version of `nnreal.mul_finset_sup` (#13512)
  chore(*/matrix): order `m` and `n` alphabetically (#13510)
  feat(analysis/calculus/specific_functions): trivial extra lemmas (#13516)
  feat(analysis): lemmas about nnnorm and nndist (#13498)
  feat(data/int/basic): add lemma `int.abs_le_one_iff` (#13513)
  feat(category_theory/limits): add characteristic predicate for zero objects (#13511)
  feat(order/filter/n_ary): Add lemma equating map₂ to map on the product (#13490)
  fix(analysis/locally_convex/balanced_hull_core): minimize import (#13450)
  feat(order/cover): define `wcovby` (#13424)
  ...
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@YaelDillies YaelDillies YaelDillies left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@berndlosert @eric-wieser @YaelDillies @leanprover-community-bot-assistant