counitAppCont — Mathlib

English

The counit is a frame homomorphism from the locale into opens of the pointed locale's PT.

Русский

Счетчик (counit) является гомоморфизмом рам из локали в множества открытых у соответствующей PT локали.

LaTeX

$$counitAppCont : FrameHom L (Opens <| PT L)$$

Lean4

/-- The counit is a frame homomorphism. -/
def counitAppCont : FrameHom L (Opens <| PT L)
    where
  toFun u := ⟨openOfElementHom L u, u, rfl⟩
  map_inf' a b := by simp
  map_top' := by simp
  map_sSup' S := by ext; simp

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