instBiheytingHomClass — Mathlib

English

The class of Biheyting homomorphisms from α to β is equipped with structure-preserving maps: sup, inf, himp, and sdiff.

Русский

Класс BiheytingHom(α,β) снабжен отображениями, сохраняющими операции sup, inf, himp и sdiff.

LaTeX

$$$\text{BiheytingHomClass}(\mathrm{BiheytingHom}(\alpha,\beta),\alpha,\beta)$ with map\_sup f = f.map\_sup',\ map\_inf f = f.map\_inf',\ map\_himp f = f.map\_himp',\ map\_sdiff f = f.map\_sdiff'$$$

Lean4

instance : BiheytingHomClass (BiheytingHom α β) α β
    where
  map_sup f := f.map_sup'
  map_inf f := f.map_inf'
  map_himp f := f.map_himp'
  map_sdiff f := f.map_sdiff'

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