English
Given a bijection between s and t and a subset s' ⊇ s and t' ⊇ t, there exists s'' ⊇ s with s'' ⊆ s' such that f maps s'' bijectively onto t'.
Русский
Если есть биекция между s и t и подмножество s' ⊇ s и t' ⊇ t, то существует s'' ⊇ s с s'' ⊆ s' и f отображает s'' биективно на t'.
LaTeX
$$$\\exists s' \\subseteq s',\\; s \\subseteq s' \\land s' \\subseteq s_1 \\land BijOn f s' t'$$$
Lean4
/-- If `f` maps `s` bijectively to `t` and a set `t'` is contained in the image of some `s₁ ⊇ s`,
then `s₁` has a subset containing `s` that `f` maps bijectively to `t'`. -/
theorem exists_extend_of_subset {t' : Set β} (h : BijOn f s t) (hss₁ : s ⊆ s₁) (htt' : t ⊆ t') (ht' : SurjOn f s₁ t') :
∃ s', s ⊆ s' ∧ s' ⊆ s₁ ∧ Set.BijOn f s' t' :=
by
obtain ⟨r, hrss, hbij⟩ := exists_subset_bijOn ((s₁ ∩ f ⁻¹' t') \ f ⁻¹' t) f
rw [image_diff_preimage, image_inter_preimage] at hbij
refine ⟨s ∪ r, subset_union_left, ?_, ?_, ?_, fun y hyt' ↦ ?_⟩
· exact union_subset hss₁ <| hrss.trans <| diff_subset.trans inter_subset_left
· rw [mapsTo_iff_image_subset, image_union, hbij.image_eq, h.image_eq, union_subset_iff]
exact ⟨htt', diff_subset.trans inter_subset_right⟩
· rw [injOn_union, and_iff_right h.injOn, and_iff_right hbij.injOn]
· refine fun x hxs y hyr hxy ↦ (hrss hyr).2 ?_
rw [← h.image_eq]
exact ⟨x, hxs, hxy⟩
exact (subset_diff.1 hrss).2.symm.mono_left h.mapsTo
rw [image_union, h.image_eq, hbij.image_eq, union_diff_self]
exact .inr ⟨ht' hyt', hyt'⟩
