toSupBotHomClass — Mathlib

English

Dual.symm preserves composition for InfTopHom morphisms.

Русский

Symm.dual сохраняет композицию для InfTopHom отображений.

LaTeX

$$$ \\mathrm{InfTopHom.dual.symm} (g \\circ f) = (\\mathrm{InfTopHom.dual.symm} g) \\circ (\\mathrm{InfTopHom.dual.symm} f) $$$

Lean4

instance (priority := 100) toSupBotHomClass [CompleteLattice α] [CompleteLattice β] [sSupHomClass F α β] :
    SupBotHomClass F α β :=
  {
    ‹sSupHomClass F α
        β› with
    map_sup := fun f a b => by
      rw [← sSup_pair, map_sSup]
      simp only [Set.image_pair, sSup_insert, sSup_singleton]
    map_bot := fun f => by rw [← sSup_empty, map_sSup, Set.image_empty, sSup_empty] }
    -- See note [lower instance priority]

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