-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(data/finset/lattice): sup'
/inf'
lemmas
#18989
Conversation
lemma sup'_product_left {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β × γ → α) : | ||
(s ×ˢ t).sup' (hs.product ht) f = s.sup' hs (λ i, t.sup' ht $ λ i', f ⟨i, i'⟩) := | ||
eq_of_forall_ge_iff $ λ a, by simp [@forall_swap _ γ] | ||
|
||
lemma sup'_product_right {t : finset γ} (hs : s.nonempty) (ht : t.nonempty) (f : β × γ → α) : | ||
(s ×ˢ t).sup' (hs.product ht) f = t.sup' ht (λ i', s.sup' hs $ λ i, f ⟨i, i'⟩) := | ||
by rw [sup'_product_left, finset.sup'_comm] |
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 assume there's some precedent for these names; can you refer to it in a --
comment?
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.
Yeah, the corresponding finset.sup
lemmas. Do you really think that's needed? I'm not going to write "See also finset.sup_x
" in the docstring of every finset.sup'_x
and vice-versa.
Otherwise LGTM. |
bors d+ |
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
Canceled. |
bors merge |
Build failed (retrying...): |
Match (most of) the lemmas between `finset.sup`/`finset.inf` and `finset.sup'`/`finset.inf'`. Also golf two proofs using `eq_of_forall_ge_iff` to make sure both APIs prove their lemmas in as closely as possible a way. Also define `finset.nontrivial` to match `set.nontrivial`.
Build failed: |
bors merge |
Canceled. |
bors merge |
Match (most of) the lemmas between `finset.sup`/`finset.inf` and `finset.sup'`/`finset.inf'`. Also golf two proofs using `eq_of_forall_ge_iff` to make sure both APIs prove their lemmas in as closely as possible a way. Also define `finset.nontrivial` to match `set.nontrivial`.
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. |
sup'
/inf'
lemmassup'
/inf'
lemmas
* 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
Match (most of) the lemmas between
finset.sup
/finset.inf
andfinset.sup'
/finset.inf'
. Also golf two proofs usingeq_of_forall_ge_iff
to make sure both APIs prove their lemmas in as closely as possible a way. Also definefinset.nontrivial
to matchset.nontrivial
.