image_le_image_iff — Mathlib

English

For an open immersion f, f'' U ≤ f'' V iff U ≤ V.

Русский

Для открытого вложения f образ подмножеств U и V удовлетворяет равенству: f(U) ≤ f(V) тогда и только тогда, когда U ≤ V.

LaTeX

$$$f ''ᵁ U \\le f ''ᵁ V \\;\\iff\\; U \\le V$$$

Lean4

theorem image_le_image_iff (f : X ⟶ Y) [IsOpenImmersion f] (U U' : X.Opens) : f ''ᵁ U ≤ f ''ᵁ U' ↔ U ≤ U' :=
  by
  refine ⟨fun h ↦ ?_, image_le_image_of_le f⟩
  rw [← preimage_image_eq f U, ← preimage_image_eq f U']
  apply preimage_le_preimage_of_le f h

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