map_strictMono — Mathlib

English

Images under a closed embedding are strictly monotone on the preorder of irreducible closeds.

Русский

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

LaTeX

$$$ \text{StrictMono}( \operatorname{IrreducibleCloseds.map}(f) ) $$$

Lean4

/-- Taking images under a closed embedding is strictly monotone on the preorder of irreducible closeds.
-/
theorem map_strictMono {f : X → Y} (hf : IsClosedEmbedding f) :
    StrictMono (IrreducibleCloseds.map hf.continuous hf.isClosedMap) := fun ⦃_ _⦄ UltV ↦
  hf.injective.image_strictMono UltV

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