[Merged by Bors] - feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup by Bergschaf · Pull Request #20328 · leanprover-community/mathlib4

Bergschaf · 2024-12-29T17:08:59Z

Himp can be expressed in terms of sSup. Does this fit into mathlib?

github-actions · 2024-12-29T17:09:52Z

PR summary 51a7682511

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ compl_eq_sSup_disjoint
+ himp_eq_sSup
+ hnot_eq_sInf_codisjoint
+ isGreatest_compl
+ isGreatest_himp
+ isLeast_hnot
+ isLeast_sdiff
+ sdiff_eq_sInf

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

eric-wieser

This holds a little more generally as

theorem isGreatest_hImp {α} [GeneralizedHeytingAlgebra α] (a b : α) : IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b) := by
  constructor
  · simp [mem_upperBounds]
  · intro a ha
    simp_all

theorem isLeast_hImp {α} [GeneralizedCoheytingAlgebra α] (a b : α) : IsLeast {w | a ≤ b ⊔ w} (a \ b) := by)
  constructor
  · simp [mem_lowerBounds]
  · intro a ha
    simp_all

where the proofs could possibly be golfed.

Perhaps @YaelDillies has opinions on how many versions of this we actually want.

YaelDillies · 2024-12-30T22:15:43Z

There you go:

theorem isGreatest_himp {α} [GeneralizedHeytingAlgebra α] (a b : α) :
    IsGreatest {w | w ⊓ a ≤ b} (a ⇨ b) := by simp [IsGreatest, mem_upperBounds]

theorem isLeast_himp {α} [GeneralizedCoheytingAlgebra α] (a b : α) : IsLeast {w | a ≤ b ⊔ w} (a \ b) := by
  simp [IsLeast, mem_lowerBounds]

and yes please add those lemmas as well as their sSup/sInf corollaries. Thanks!

Bergschaf · 2024-12-31T09:40:13Z

Thank you for the review!
I added these two in the middle:

lemma isGreatest_sSup {α} [CompleteSemilatticeSup α] (a : α) (s : Set α) :
  IsGreatest s a → sSup s = a :=
    fun h ↦ IsLUB.sSup_eq (IsGreatest.isLUB h)

lemma isLeast_sInf {α} [CompleteSemilatticeInf α] (a : α) (s : Set α) :
  IsLeast s a → sInf s = a :=
    fun h ↦ IsGLB.sInf_eq (IsLeast.isGLB h)

Are they to trivial or should I do a seperate PR with these two (probably in a different file)?

Mathlib/Order/CompleteBooleanAlgebra.lean

Mathlib/Order/Bounds/Basic.lean

eric-wieser · 2025-01-03T18:03:20Z

Mathlib/Order/Bounds/Basic.lean


 end LinearOrder

-theorem isGreatest_himp [GeneralizedHeytingAlgebra α] (a b : α) :


I think these were better explicit.

What's your argument for this? Mine for them being implicit is that they likely will never be used in a proof term that doesn't have enough context to prevent unification, and if ever that happens it would be better to add a type ascription rather than adding explicit arguments to some lemma in the middle of the proof term

I can see this being the type of thing where I'd want to write have := isGreatest_himp (foo x) (bar x), and then think a little using the goal state before proceeding. I don't think that _s within a proof term are likely to matter, especially since probably nothing much is going to use these lemmas.

Mathlib/Order/Bounds/Basic.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Bergschaf · 2025-01-04T13:59:58Z

I used eric's golf and the explicit arguments. Is this fine?

Mathlib/Order/Bounds/Basic.lean

eric-wieser

Thanks!

YaelDillies · 2025-01-31T16:11:56Z

Sorry, looks like we dropped the ball here.

maintainer merge

github-actions · 2025-01-31T16:12:17Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

bryangingechen

Thanks!
bors r+

Co-authored-by: Bergschaf <86738237+Bergschaf@users.noreply.github.com>

mathlib-bors · 2025-01-31T17:05:35Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

Co-authored-by: Bergschaf <86738237+Bergschaf@users.noreply.github.com>

himp eq

34ae9b4

Bergschaf added the RFC Request for comment label Dec 29, 2024

github-actions bot added the t-order Order theory label Dec 29, 2024

eric-wieser reviewed Dec 30, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 30, 2024

commit

5811458

Bergschaf removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 31, 2024

YaelDillies reviewed Dec 31, 2024

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Dec 31, 2024

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes. and removed RFC Request for comment labels Dec 31, 2024

update

a8b18bb

Bergschaf added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Dec 31, 2024

eric-wieser reviewed Dec 31, 2024

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Dec 31, 2024

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Dec 31, 2024

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 31, 2024

Bergschaf added 2 commits December 31, 2024 12:18

switch direction

1a8bb74

move to coframe section

e16c581

Bergschaf removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 31, 2024

eric-wieser reviewed Dec 31, 2024

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

Bergschaf added 3 commits December 31, 2024 12:36

.symm

f520c64

move

ffaf896

x

c1bc1de

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 31, 2024

Bergschaf requested a review from eric-wieser January 3, 2025 07:18

forgor

fe4ddc1

YaelDillies reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/CompleteBooleanAlgebra.lean Outdated Show resolved Hide resolved

YaelDillies reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/Bounds/Basic.lean Show resolved Hide resolved

commit

8ed2529

eric-wieser reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/Bounds/Basic.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 3, 2025

View reviewed changes

YaelDillies reviewed Jan 3, 2025

View reviewed changes

Mathlib/Order/Bounds/Basic.lean Outdated Show resolved Hide resolved

Bergschaf and others added 2 commits January 4, 2025 09:26

Update Mathlib/Order/Bounds/Basic.lean

e02cd85

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

commit

fa93e2f

Bergschaf requested review from YaelDillies and eric-wieser January 4, 2025 14:00

eric-wieser reviewed Jan 4, 2025

View reviewed changes

Mathlib/Order/Bounds/Basic.lean Outdated Show resolved Hide resolved

eric-wieser approved these changes Jan 4, 2025

View reviewed changes

style

51a7682

YaelDillies approved these changes Jan 4, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 31, 2025

bryangingechen approved these changes Jan 31, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 31, 2025

mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2025

feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)

c02933f

Co-authored-by: Bergschaf <86738237+Bergschaf@users.noreply.github.com>

mathlib-bors bot changed the title ~~feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup~~ [Merged by Bors] - feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the himp_eq branch January 31, 2025 17:05

jt496 pushed a commit that referenced this pull request Feb 3, 2025

feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328)

6df62ab

Co-authored-by: Bergschaf <86738237+Bergschaf@users.noreply.github.com>


		end LinearOrder

		theorem isGreatest_himp [GeneralizedHeytingAlgebra α] (a b : α) :

Conversation

Bergschaf commented Dec 29, 2024 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 29, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 51a7682511

Import changes for modified files

Declarations diff

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies commented Dec 30, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Bergschaf commented Dec 31, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jan 3, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Bergschaf commented Jan 4, 2025

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

YaelDillies commented Jan 31, 2025

Uh oh!

github-actions bot commented Jan 31, 2025

Uh oh!

bryangingechen left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Bergschaf commented Dec 29, 2024 •

edited by eric-wieser

Loading

github-actions bot commented Dec 29, 2024 •

edited

Loading

YaelDillies commented Dec 30, 2024 •

edited

Loading

Bergschaf commented Dec 31, 2024 •

edited

Loading