ι_app — Mathlib

English

The top-level application of ι matches the presheaf map on opens.

Русский

Применение верхнего уровня ι согласуется с отображением предшаблонов на открытых множествах.

LaTeX

$$U.ι.appTop = X.presheaf.map (homOfLE (x := U.ι ''ᵁ ⊤) le_top).op$$

Lean4

@[simp]
theorem ι_app (V) : U.ι.app V = X.presheaf.map (homOfLE (x := U.ι ''ᵁ U.ι ⁻¹ᵁ V) (Set.image_preimage_subset _ _)).op :=
  rfl

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