map_id_obj' — Mathlib

English

In the opposite OpenNhds category, the identity morphism acts as identity on the unop object.

Русский

В противоположной категории OpenNhds идентичность действует как тождественный переход на объекте unop.

LaTeX

$$map_id_obj_unop (x) (U) : (map (id X) x).obj (unop U) = unop U$$

Lean4

@[simp]
theorem map_id_obj' (x : X) (U) (p) (q) : (map (𝟙 X) x).obj ⟨⟨U, p⟩, q⟩ = ⟨⟨U, p⟩, q⟩ :=
  rfl

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