English
The construction that assigns to a Frame α a MinimalAxioms α structure, preserving the inf-sup behavior.
Русский
Построение, сопоставляющее каждому Frame α структуру MinimalAxioms α, сохраняющую поведение inf-sup.
LaTeX
$$$\mathrm{of} : \mathrm{Frame} \ α \to \mathrm{MinimalAxioms} \ α$$$
Lean4
/-- Construct a frame instance using the minimal amount of work needed.
This sets `a ⇨ b := sSup {c | c ⊓ a ≤ b}` and `aᶜ := a ⇨ ⊥`. -/
-- See note [reducible non-instances]
abbrev ofMinimalAxioms (minAx : MinimalAxioms α) : Frame α
where
__ := minAx
compl a := sSup {c | c ⊓ a ≤ ⊥}
himp a b := sSup {c | c ⊓ a ≤ b}
le_himp_iff _ b c := ⟨fun h ↦ (inf_le_inf_right _ h).trans (by simp [minAx.sSup_inf_eq]), fun h ↦ le_sSup h⟩
himp_bot _ := rfl
