English
Let e be a bijection between α and β, with s ⊆ α and t ⊆ β such that for every a, e(a) ∈ t if and only if a ∈ s. Then the restriction of e to s is a bijection from s onto t.
Русский
Пусть e: α → β — биекция, задана пары подмножеств s ⊆ α и t ⊆ β такие, что для каждого a справедливо e(a) ∈ t тогда и только тогда, когда a ∈ s. Тогда ограничение e на s представляет собой биекцию s → t.
LaTeX
$$$\bigl(\forall a,\ e(a) \in t \iff a \in s\bigr) \Rightarrow \mathrm{BijOn}(e,s,t)$$$
Lean4
protected theorem bijOn (h : ∀ a, e a ∈ t ↔ a ∈ s) : BijOn e s t :=
e.bijOn' (fun _ ↦ (h _).2) fun b hb ↦ (h _).1 <| by rwa [apply_symm_apply]
