[Merged by Bors] - chore(order/liminf_limsup): Generalise and move lemmas #18628
Conversation
YaelDillies
added
awaiting-review
| /--Adding a point to a set preserves its boundedness below.-/ | ||
| @[simp] lemma bdd_below_insert [semilattice_inf γ] (a : γ) {s : set γ} : | ||
| @[simp] lemma bdd_below_insert [is_directed α (≥)] {s : set α} {a : α} : | ||
| bdd_below (insert a s) ↔ bdd_below s := | ||
| by simp only [insert_eq, bdd_below_union, bdd_below_singleton, true_and] | ||
|
|
||
| lemma bdd_below.insert [semilattice_inf γ] (a : γ) {s : set γ} (hs : bdd_below s) : | ||
| bdd_below (insert a s) := | ||
| (bdd_below_insert a).2 hs | ||
| lemma bdd_below.insert [is_directed α (≥)] {s : set α} (a : α) : | ||
| bdd_below s → bdd_below (insert a s) := | ||
| bdd_below_insert.2 |
There was a problem hiding this comment.
For PRs that need forward-porting, it would really be best not to make stylistic changes. Can't you just replace semilattice_inf γ with is_directed γ (≥) (and fix docstrings) and not touch anything else?
There was a problem hiding this comment.
Especially for things like reordering implicit arguments, as you've done here
There was a problem hiding this comment.
What stylistic changes have I made? I made the explicit argument a implicit. This is not stylistic.
There was a problem hiding this comment.
It borders on stylistic, given the PR description makes no mention of it. I should have said "aesthetic" though I guess.
You also changed γ for α, moved things after the colon, and reordered some arguments. These are all things that just make the forward-port review harder. Note that reordering arguments is particularly risky because it's hard to spot skimming a diff, and the #align machinery doesn't do well if we screw up the forward-port.
There was a problem hiding this comment.
Now mentioned in the PR description. The only reason \gamma was used was because \alpha is already declared to be a preorder in the section.
kim-em
added
the
modifies-synchronized-file
eric-wieser
added
the
not-too-late
|
bors d+ Please merge whenever you think is a good moment to be able to do the forward port promptly. :-) |
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
github-actions
bot
added
delegated
|
bors merge |
Generalise lemmas from semilattices to codirected orders. Move topology-less lemmas from `topology.algebra.order.liminf_limsup` to `order.liminf_limsup`. Also turn arguments to `bdd_above_insert` and friends implicit.
|
Build failed (retrying...): |
Generalise lemmas from semilattices to codirected orders. Move topology-less lemmas from `topology.algebra.order.liminf_limsup` to `order.liminf_limsup`. Also turn arguments to `bdd_above_insert` and friends implicit.
|
Build failed: |
|
bors merge |
Generalise lemmas from semilattices to codirected orders. Move topology-less lemmas from `topology.algebra.order.liminf_limsup` to `order.liminf_limsup`. Also turn arguments to `bdd_above_insert` and friends implicit.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
* commit '65a1391a0106c9204fe45bc73a039f056558cb83': (12443 commits)
feat(data/{list,multiset,finset}/*): `attach` and `filter` lemmas (leanprover-community#18087)
feat(combinatorics/simple_graph): More clique lemmas (leanprover-community#19203)
feat(measure_theory/order/upper_lower): Order-connected sets in `ℝⁿ` are measurable (leanprover-community#16976)
move old README.md to OLD_README.md
doc: Add a warning mentioning Lean 4 to the readme (leanprover-community#19243)
feat(topology/metric_space): diameter of pointwise zero and addition (leanprover-community#19028)
feat(topology/algebra/order/liminf_limsup): Eventual boundedness of neighborhoods (leanprover-community#18629)
feat(probability/independence): Independence of singletons (leanprover-community#18506)
feat(combinatorics/set_family/ahlswede_zhang): Ahlswede-Zhang identity, part I (leanprover-community#18612)
feat(data/finset/lattice): `sup'`/`inf'` lemmas (leanprover-community#18989)
chore(order/liminf_limsup): Generalise and move lemmas (leanprover-community#18628)
feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for abelian categories (leanprover-community#17926)
feat(data/sum/interval): The lexicographic sum of two locally finite orders is locally finite (leanprover-community#11352)
feat(analysis/convex/proj_Icc): Extending convex functions (leanprover-community#18797)
feat(algebraic_topology/dold_kan): The Dold-Kan equivalence for pseudoabelian categories (leanprover-community#17925)
feat(measure_theory/measure/haar_quotient): the Unfolding Trick (leanprover-community#18863)
feat(linear_algebra/orientation): add `orientation.reindex` (leanprover-community#19236)
feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths (leanprover-community#17828)
feat(set_theory/game/pgame): small sets of pre-games / games / surreals are bounded (leanprover-community#15260)
feat(tactic/positivity): Extension for `ite` (leanprover-community#17650)
...
# Conflicts:
# README.md
Generalise lemmas from semilattices to codirected orders. Move topology-less lemmas from
topology.algebra.order.liminf_limsuptoorder.liminf_limsup. Also turn arguments tobdd_above_insertand friends implicit.