image — Mathlib

English

Same as image_inter with the explicit bound and proof structure.

Русский

Та же формулировка, что и image_inter, с явной структурой доказательства.

LaTeX

$$$ \\operatorname{InjOn} f u \\land s \\subseteq u \\land t \\subseteq u \\Rightarrow f '' (s \\cap t) = f '' s \\cap f '' t$$$

Lean4

theorem image (h : s.InjOn f) : s.powerset.InjOn (image f) := fun s₁ hs₁ s₂ hs₂ h' ↦ by
  rw [← h.preimage_image_inter hs₁, h', h.preimage_image_inter hs₂]

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