sdiff_singleton — Mathlib

English

If f is a bijection from S to T and a ∈ S, then f restricts to a bijection from S \\ {a} to T \\ {f(a)}.

Русский

Если f биекция от S на T и a ∈ S, тогда ограничение f на S \\ {a} образует биекцию с T \\ {f(a)}.

LaTeX

$$$$ \\text{BijOn } f S T \\land a \\in S \\Rightarrow \\text{BijOn } f (S \\{a}) (T \\{f(a)\\}). $$$$

Lean4

theorem sdiff_singleton (h₁ : BijOn f s t) (h₂ : a ∈ s) : BijOn f (s \ { a }) (t \ {f a}) :=
  by
  convert h₁.subset_left diff_subset
  simp [h₁.injOn.image_diff, h₁.image_eq, h₂, inter_eq_self_of_subset_right]

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