exists_image_eq_and_injOn — Mathlib

English

There exists a subset u of s such that f maps u onto the same image as s and f is injective on u.

Русский

Существует подмножество u ⊆ s, такое что образ f на u совпадает с образом f на s, и f инъективна на u.

LaTeX

$$$\\exists u \\subseteq s, (image f u) = (image f s) \\land InjOn f u$$$

Lean4

theorem exists_image_eq_and_injOn : ∃ u, f '' u = f '' s ∧ InjOn f u :=
  let ⟨u, _, hfu⟩ := exists_subset_bijOn s f
  ⟨u, hfu.image_eq, hfu.injOn⟩

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