instCoframe — Mathlib

English

There is an instance that endows the collection of filters with a Coframe structure via the minimal axioms.

Русский

Существует экземпляр, наделяющий множество фильтров структурой кофрейма через минимальные аксиомы.

LaTeX

$$$ \text{instance } \mathrm{Coframe}(\mathrm{Filter}\; \alpha) : \mathrm{Coframe}(\mathrm{Filter}\; \alpha) $$$

Lean4

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

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