map_radical — Mathlib

English

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 map_radical (f : α ≃o β) : f (Order.radical α) = Order.radical β :=
  by
  unfold Order.radical
  simp only [OrderIso.map_iInf]
  fapply Equiv.iInf_congr
  · exact f.toEquiv
  · simp

Похожие утверждения