instCoframe — Mathlib

English

The collection of closed sets is endowed with a Coframe structure, i.e., a Coframe on Closeds α; concretely, it is built from the minimal axioms.

Русский

Множество замкнутых множеств снабжается структурой Coframe, то есть Coframe на Closeds α, построенное из минимальных аксиом.

LaTeX

$$$\mathrm{instCoframe} : \mathrm{Coframe}(\mathrm{Closeds}(\alpha)).$$$

Lean4

instance instCoframe : Coframe (Closeds α) :=
  .ofMinimalAxioms coframeMinimalAxioms

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