what sort of lattice is needed?

Stream: Is there code for X?

[Scott Morrison]

What assumptions on α are required to make this example provable?

import order.bounded_lattice

example {α : Type*} [bounded_lattice α] (a b : α) (w : a ⊓ b = ⊥) (h : a ⊔ b = a) : b = ⊥ :=
sorry

[Bryan Gin-ge Chen]

This works:

import order.bounded_lattice

example {α : Type*} [bounded_lattice α] (a b : α) (w : a ⊓ b = ⊥) (h : a ⊔ b = a) : b = ⊥ :=
begin
  rw [←w, right_eq_inf],
  rwa sup_eq_left at h,
end

[Scott Morrison]

Oh! I was thinking that a stronger hypothesis was necessary! Thanks.

[Scott Morrison]

Another lattice theory question:

import order.bounded_lattice

example {α : Type*} [bounded_lattice α] (a b c : α) (w : a ⊓ b = ⊥) (h : (a ⊔ b) ⊓ c = ⊥) :
  a ⊓ (b ⊔ c) = ⊥ :=
sorry

You're allowed to strengthen the hypotheses, but I'd like it to work for submodule R M.

[Hanting Zhang]

I haven't looked too closely, but this reminds me of docs#disjoint.disjoint_sup_right_of_disjoint_sup_left

[Hanting Zhang]

import order.bounded_lattice

example {α : Type*} [bounded_lattice α] [is_modular_lattice α] (a b c : α) (hab : a ⊓ b = ⊥)
  (h : (a ⊔ b) ⊓ c = ⊥) : a ⊓ (b ⊔ c) = ⊥ :=
begin
  have disjoint_def : ∀ {a b : α}, disjoint a b ↔ a ⊓ b = ⊥,
  { intros a b, rw [disjoint, eq_bot_iff], },
  rw ← disjoint_def,
  rw ← disjoint_def at hab,
  rw ← disjoint_def at h,
  exact disjoint.disjoint_sup_right_of_disjoint_sup_left hab h,
end

[Hanting Zhang]

Actually it's on the nose lol

[Scott Morrison]

Thanks very much. I can maths-prove this sort of thing by drawing a little picture of hyperplanes, but when it comes to doing the reverse mathematics of working out what sort of lattice is relevant, I seem to be helpless. :-)

[Eric Wieser]

I think your disjoint_def exists already as docs#disjoint_iff