instCoheytingHomClass — Mathlib

English

The collection of Coheyting homomorphisms from α to β forms a structure-preserving class with maps that preserve join, meet, top, and a residual operation.

Русский

Множество когейтингов-гомоморфизмов от α к β образует структуру, сохраняющую операции объединения, пересечения, максимум и остаток.

LaTeX

$$$\text{CoheytingHomClass}(\mathrm{CoheytingHom}(\alpha,\beta),\alpha,\beta)$ with map\_sup f = f.map\_sup',\ map\_inf f = f.map\_inf',\ map\_top f = f.map\_top',\ map\_sdiff = \text{CoheytingHom.map\_sdiff}\'\,,$$$

Lean4

instance : CoheytingHomClass (CoheytingHom α β) α β
    where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'
  map_top f := f.map_top'
  map_sdiff := CoheytingHom.map_sdiff'

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