English
Let f : α → β, S ⊆ α, T ⊆ β, a ∈ α. If a ∉ S and f(a) ∉ T, then f induces a bijection between S ∪ {a} and T ∪ {f(a)} if and only if f induces a bijection between S and T.
Русский
Пусть f: α → β, S ⊆ α, T ⊆ β, a ∈ α. Если a ∉ S и f(a) ∉ T, то отображение f ограниченное на S ∪ {a} биективно отображает S ∪ {a} на T ∪ {f(a)} тогда и только тогда, когда ограничение f на S биективно отображает S на T.
LaTeX
$$$$ \\text{If } a\\notin S \\text{ and } f(a)\\notin T, \\quad \\text{BijOn } f (S \\cup \\{a\\}) (T \\cup \\{f(a)\\}) \\;\\Longleftrightarrow\\; \\text{BijOn } f S T.$$$$
Lean4
theorem insert_iff (ha : a ∉ s) (hfa : f a ∉ t) : BijOn f (insert a s) (insert (f a) t) ↔ BijOn f s t
where
mp
h := by
have := congrArg (· \ {f a}) (image_insert_eq ▸ h.image_eq)
simp only [mem_singleton_iff, insert_diff_of_mem] at this
rw [diff_singleton_eq_self hfa, diff_singleton_eq_self] at this
· exact ⟨by simp [← this, mapsTo_iff_image_subset], h.injOn.mono (subset_insert ..), by simp [← this, surjOn_image]⟩
simp only [mem_image, not_exists, not_and]
intro x hx
rw [h.injOn.eq_iff (by simp [hx]) (by simp)]
exact ha ∘ (· ▸ hx)
mpr
h := by
repeat rw [insert_eq]
refine (bijOn_singleton.mpr rfl).union h ?_
simp only [singleton_union, injOn_insert fun x ↦ (hfa (h.mapsTo x)), h.injOn, mem_image, not_exists, not_and,
true_and]
exact fun _ hx h₂ ↦ hfa (h₂ ▸ h.mapsTo hx)
