toCoframe — Mathlib

English

From a MinimalAxioms structure for CompleteDistribLattice one obtains a Coframe MinimalAxioms on α with the required translations between infimum/supremum and their frame counterparts.

Русский

Из структуры MinimalAxioms для CompleteDistribLattice получается Coframe MinimalAxioms на α со связями между inf и sup и их аналогами в рамке.

LaTeX

$$$\\text{toCoframe}: \\text{CompleteDistribLattice.MinimalAxioms } α \\to \\text{Coframe.MinimalAxioms } α$$$

Lean4

/-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Coframe`. -/
abbrev toCoframe : Coframe.MinimalAxioms α where __ := minAx

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