English
From a minimal-axioms structure for α one can build a Coframe α by setting hnot a = sInf{c | ⊤ ≤ a ⊔ c} and sdiff a b = sInf{c | a ≤ b ⊔ c}, together with the appropriate compatibility conditions.
Русский
Из структуры с минимальными аксиомами для α можно получить кофрейм α, задавая hnot a = inf{c | ⊤ ≤ a ⊔ c} и sdiff a b = inf{c | a ≤ b ⊔ c}, соблюдая необходимые условия совместимости.
LaTeX
$$$\\text{ofMinimalAxioms}(minAx) = \\text{Coframe.MinimalAxioms } α \\text{ with } hnot(a) = \\inf\\{c \\mid \\top \\le a \\lor c\\}, \\; \\mathrm{sdiff}(a,b) = \\inf\\{c \\mid a \\le b \\lor c\\},$$$
Lean4
/-- The `Order.Coframe.MinimalAxioms` element corresponding to a frame. -/
def of [Coframe α] : MinimalAxioms α where
__ := ‹Coframe α›
iInf_sup_le_sup_sInf a s := _root_.sup_sInf_eq.ge
