English
If f maps s bijectively to t and t' is a superset of t contained in range f, then there exists s' such that s ⊆ s' and f maps s' bijectively to t'.
Русский
Если f отображает s биективно в t, а t' ⊇ t и t' ⊆ range f, то существует s' ⊇ s с биективным отображением f на t'.
LaTeX
$$$ h: BijOn f s t, \\; s' ⊇ s, t' ⊇ t, t' ⊆ range f \\Rightarrow \\exists s', s ⊆ s' ∧ BijOn f s' t'$$$
Lean4
/-- If `f` maps `s` bijectively to `t`, and `t'` is a superset of `t` contained in the range of `f`,
then `f` maps some superset of `s` bijectively to `t'`. -/
theorem exists_extend {t' : Set β} (h : BijOn f s t) (htt' : t ⊆ t') (ht' : t' ⊆ range f) :
∃ s', s ⊆ s' ∧ BijOn f s' t' := by simpa using h.exists_extend_of_subset (subset_univ s) htt' (by simpa [SurjOn])
