isOpenEmbedding_of_le — Mathlib

English

If U ≤ V as opens, the inclusion map U → α is an open embedding.

Русский

Если U ⊆ V как открытые множества, то включение U → α является открытым вложением.

LaTeX

$$$ IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i) $$$

Lean4

theorem isOpenEmbedding_of_le {U V : Opens α} (i : U ≤ V) :
    IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i)
    where
  toIsEmbedding := .inclusion i
  isOpen_range := by
    rw [Set.range_inclusion i]
    exact U.isOpen.preimage continuous_subtype_val

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