injOn_preimage — Mathlib

English

If B is a family of subsets of the range of f, then the preimage map f⁻¹ on B is injective on B.

Русский

Если B — множество подмножеств образа f, то отображение предобраза f⁻¹ на B инъективно.

LaTeX

$$$ \\forall B \\subseteq \\mathcal P(\\operatorname{range} f), \\operatorname{InjOn}(\\operatorname{preimage} f) B$$

Lean4

theorem injOn_preimage {B : Set (Set β)} (hB : B ⊆ 𝒫 range f) : InjOn (preimage f) B := fun _ hs _ ht hst =>
  (preimage_eq_preimage' (hB hs) (hB ht)).1 hst

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