exists_subset_injOn_image_eq — Mathlib

English

If a surjective relation on subsets exists, there is a subset u of s that is contained in s, with f restricted to u injective and f''u = t.

Русский

Если существует подмножество, на котором ограничение f инъективно, образ которого совпадает с заданным t.

LaTeX

$$$\\exists u \\subseteq s, u \\ InjOn f u \\land f '' u = t$$$

Lean4

/-- If `t ⊆ f '' s`, there exists a preimage of `t` under `f` contained in `s` such that
`f` restricted to `u` is injective. -/
theorem exists_subset_injOn_image_eq (hfs : s.SurjOn f t) : ∃ u ⊆ s, u.InjOn f ∧ f '' u = t :=
  by
  choose x hmem heq using hfs
  exact ⟨range (fun a : t ↦ x a.2), by grind, fun _ ↦ by grind, by aesop⟩

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