toFrame — Mathlib

English

Turning minimal-axioms for a complete distributive lattice into a Frame.MinimalAxioms on α yields a canonical frame-like structure compatible with the given infimum and supremum operations.

Русский

Преобразование минимальных аксиом для полной распределимой решетки в структуру Frame.MinimalAxioms на α образует каноническую структуру, совместимую с операциями inf и sup.

LaTeX

$$$\\text{toFrameMinimalAxioms}: \\text{CompleteDistribLattice.MinimalAxioms } α \\to \\text{Frame.MinimalAxioms } α$$$

Lean4

/-- Turn minimal axioms for `CompleteDistribLattice` into minimal axioms for `Order.Frame`. -/
abbrev toFrame : Frame.MinimalAxioms α :=
  minAx.toFrameMinimalAxioms

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