English
As above: In a coatomic lattice α, if a ⊔ radical(α) = ⊤, then a = ⊤.
Русский
Как выше: в коатомной решётке α, если a ⊔ radical(α) = ⊤, то a = ⊤.
LaTeX
$$$\text{In a coatomic lattice } \alpha:\ a \lor \operatorname{radical}(\alpha) = \top \Rightarrow a = \top.$$$
Lean4
theorem radical_nongenerating [IsCoatomic α] {a : α} (h : a ⊔ radical α = ⊤) : a = ⊤ := by
-- Since the lattice is coatomic, either `a` is already the top element,
-- or there is a coatom above it.
obtain (rfl | w) := eq_top_or_exists_le_coatom a
· -- In the first case, we're done, this was already the goal.
rfl
· obtain ⟨m, c, le⟩ := w
have q : a ⊔ radical α ≤ m :=
sup_le le
(radical_le_coatom c)
-- Now note that `a ⊔ radical α ≤ m` since both `a ≤ m` and `radical α ≤ m`.
rw [h, top_le_iff] at q
simpa using c.1 q
