inclusion — Mathlib

English

Given a subset relation and some openness condition, the inclusion map is an open embedding.

Русский

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

LaTeX

$$$\\forall \\text{hst},\\; \\text{IsOpenEmbedding}(\\text{Set.inclusion}(hst)).$$$

Lean4

protected theorem inclusion (hst : s ⊆ t) (hs : IsOpen (t ↓∩ s)) : IsOpenEmbedding (inclusion hst)
    where
  toIsEmbedding := .inclusion _
  isOpen_range := by rwa [range_inclusion]

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