English
There is a functorial passage from minimal-axioms of α to a Coframe structure on α, preserving infimum and supremum relations via the defined hnot and sdiff operations.
Русский
Существует переход от минимальных аксиом к структуре кофрейма на α, сохраняющий отношения Inf и Sup через заданные операции hnot и sdiff.
LaTeX
$$$\\text{toCoframe}:\\text{MinimalAxioms } α \\to \\text{Coframe.MinimalAxioms } α$ with the defining relations as above.$$
Lean4
/-- Construct a coframe instance using the minimal amount of work needed.
This sets `a \ b := sInf {c | a ≤ b ⊔ c}` and `￢a := ⊤ \ a`. -/
-- See note [reducible non-instances]
abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : Coframe α
where
__ := minAx
hnot a := sInf {c | ⊤ ≤ a ⊔ c}
sdiff a b := sInf {c | a ≤ b ⊔ c}
sdiff_le_iff a b _ := ⟨fun h ↦ (sup_le_sup_left h _).trans' (by simp [minAx.sup_sInf_eq]), fun h ↦ sInf_le h⟩
top_sdiff _ := rfl
