ι_image_homOfLE_le_ι_image — Mathlib

English

The LE maps between opens preserve images under inclusions.

Русский

Преобразования LE между открытыми сохраняют образы при включениях.

LaTeX

$$$ U.ι \\text{ image } (X.homOfLE e) \\subseteq V.ι \\text{ image } W $$$

Lean4

theorem ι_image_homOfLE_le_ι_image {U V : X.Opens} (e : U ≤ V) (W : Opens V) :
    U.ι ''ᵁ (X.homOfLE e ⁻¹ᵁ W) ≤ V.ι ''ᵁ W :=
  by
  simp only [← SetLike.coe_subset_coe, IsOpenMap.coe_functor_obj, Set.image_subset_iff, Scheme.homOfLE_base,
    Opens.map_coe]
  rintro _ h
  exact ⟨_, h, rfl⟩

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