infLELeft — Mathlib

English

There is a natural inclusion functor from OpenNhds x to Opens X, sending each neighborhood to its underlying open set of the ambient space.

Русский

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

LaTeX

$$inclusion (x) : OpenNhds x ⥤ Opens X$$

Lean4

/-- The inclusion `U ⊓ V ⟶ U` as a morphism in the category of open sets. -/
def infLELeft {x : X} (U V : OpenNhds x) : U ⊓ V ⟶ U :=
  homOfLE inf_le_left

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