English
From a Frame α one obtains a Locale by taking the opposite of the frame's underlying lattice: Locale.of α = op (Frm.of α).
Русский
Из кадра α получают локаль, взяв противоположную структуру базиса кадра: Locale.of α = op(Frm.of α).
LaTeX
$$$\operatorname{Locale}(\alpha)=\operatorname{op}(\operatorname{Frm.of}(\alpha))$$$
Lean4
/-- Construct a bundled `Locale` from a `Frame`. -/
def of (α : Type*) [Frame α] : Locale :=
op <| Frm.of α