feat (order/modular_lattice): modular_lattice as extension of lattice #7539
Conversation
Seeram
commented
May 6, 2021
Seeram
commented
| @@ -36,6 +36,9 @@ variable {α : Type*} | |||
| class is_modular_lattice α [lattice α] : Prop := | |||
| (sup_inf_le_assoc_of_le : ∀ {x : α} (y : α) {z : α}, x ≤ z → (x ⊔ y) ⊓ z ≤ x ⊔ (y ⊓ z)) | |||
|
|
|||
| class modular_lattice α extends lattice α := | |||
| (modular_law: ∀ (x u v : α ), (x ≤ u) → u ⊓ (v ⊔ x) = (u ⊓ v) ⊔ x ) | |||
There was a problem hiding this comment.
I don't think this class is a good idea - it means you need a new class to talk about modular bounded lattices, modular complete lattices, ...
What was the reason you added it?
| namespace modular_lattice | ||
|
|
||
| theorem diamond_isomorphism | ||
| [modular_lattice α] {u v w x y : α} : |
There was a problem hiding this comment.
Instead of a new class, the existing one should work fine
| [modular_lattice α] {u v w x y : α} : | |
| [lattice α] [is_modular_lattice α] {u v w x y : α} : |
| { rw modular_lattice.modular_law, | ||
| exact sup_eq_right.mpr h3, | ||
| exact h1 }, | ||
| { rw ← modular_lattice.modular_law, |
There was a problem hiding this comment.
| { rw ← modular_lattice.modular_law, | |
| { rw ← inf_sup_assoc_of_le, |
Or similar, with the changes I suggest above
eric-wieser
added
awaiting-author
|
|
||
| theorem diamond_isomorphism | ||
| [modular_lattice α] {u v w x y : α} : | ||
| (x ≤ u) → (x ≥ v) → (x ≥ u ⊓ v) → (x ≤ u ⊔ v) → u ⊓ (v ⊔ x) = x ∧ (x ⊓ u) ⊔ v = x := |
There was a problem hiding this comment.
Mathlib almost never uses ≥:
| (x ≤ u) → (x ≥ v) → (x ≥ u ⊓ v) → (x ≤ u ⊔ v) → u ⊓ (v ⊔ x) = x ∧ (x ⊓ u) ⊔ v = x := | |
| (x ≤ u) → (v ≤ x) → (u ⊓ v ≤ x) → (x ≤ u ⊔ v) → u ⊓ (v ⊔ x) = x ∧ (x ⊓ u) ⊔ v = x := |
| { rw modular_lattice.modular_law, | ||
| exact sup_eq_right.mpr h3, | ||
| exact h1 }, |
There was a problem hiding this comment.
This half of the proof only uses h1 and h3, while the other branch only uses h2 and h4. This suggests to me that this should be two different lemmas not a single lemma.
|
@YaelDillies Do you mind posting a comment summarizing the reason(s) for closing the PR? |
|
There are too many types of modular lattices for us to insert them in the order hierarchy. Instead, I envision Prop-valued mixins as the way to go. See #11602 |
