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/cover): define wcovby #13424

Closed
wants to merge 11 commits into from

Conversation

fpvandoorn
Copy link
Member

  • This defines the reflexive closure of covby, which I call wcovby ("weakly covered by")
  • This is useful, since some results about covby still hold for wcovby.
  • Use wcovby in the proofs of the properties for covby.
  • Also define wcovby_insert (the motivating example, since I really want (wcovby_insert _ _).eq_or_eq)

Open in Gitpod

@fpvandoorn fpvandoorn added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Apr 13, 2022
@fpvandoorn fpvandoorn requested a review from urkud April 13, 2022 14:47
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Apr 13, 2022
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

Thanks a lot, this looks great!

Could you add the following?

instance : is_nonstrict_strict_order α (⩿) (⋖)

You could even go as far as providing the lt_iff_le_and_ne-like lemmas for is_nonstrict_strict_order first, then deduce the -< and ⩿- ones.

src/order/cover.lean Outdated Show resolved Hide resolved
src/order/cover.lean Outdated Show resolved Hide resolved
src/order/cover.lean Outdated Show resolved Hide resolved
src/order/cover.lean Outdated Show resolved Hide resolved
src/order/cover.lean Outdated Show resolved Hide resolved
@fpvandoorn fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 13, 2022
@YaelDillies
Copy link
Collaborator

Can you also prove that a ⩿ order.succ a and order.pred a ⩿ a?

@fpvandoorn fpvandoorn removed the request for review from urkud April 14, 2022 09:31
@fpvandoorn fpvandoorn added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 14, 2022
src/order/cover.lean Outdated Show resolved Hide resolved
src/order/cover.lean Show resolved Hide resolved
@fpvandoorn fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Apr 14, 2022
@fpvandoorn fpvandoorn added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 14, 2022
@fpvandoorn fpvandoorn requested a review from YaelDillies April 15, 2022 08:30
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

LGTM

src/order/cover.lean Outdated Show resolved Hide resolved
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 19, 2022
bors bot pushed a commit that referenced this pull request Apr 19, 2022
* This defines the reflexive closure of `covby`, which I call `wcovby` ("weakly covered by")
* This is useful, since some results about `covby` still hold for `wcovby`. 
* Use `wcovby` in the proofs of the properties for `covby`.
* Also define `wcovby_insert` (the motivating example, since I really want `(wcovby_insert _ _).eq_or_eq`)
@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/cover): define wcovby [Merged by Bors] - feat(order/cover): define wcovby Apr 19, 2022
@bors bors bot closed this Apr 19, 2022
@bors bors bot deleted the fpvandoorn/cover branch April 19, 2022 15:52
Julian added a commit that referenced this pull request Apr 21, 2022
* 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.
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants