English
If a square commutes and f induces a bijection on s to t, then g induces a bijection on p1(s) to p2(t).
Русский
Если квадрат коммутирует и f индуцирует биекцию на s→t, то g индуцирует биекцию между p1(s) и p2(t).
LaTeX
$$$\\forall a, p_2(f(a))=g(p_1(a)) \\land \\text{BijOn}(f,s,t) \\land \\text{InjOn}(g,(p_1''s)) \\Rightarrow \\text{BijOn}(g,(p_1''s),(p_2''t))$$$
Lean4
/-- If we have a commutative square
```
α --f--> β
| |
p₁ p₂
| |
\/ \/
γ --g--> δ
```
and `f` induces a bijection from `s : Set α` to `t : Set β`, then `g`
induces a bijection from the image of `s` to the image of `t`, as long as `g` is
is injective on the image of `s`.
-/
theorem bijOn_image_image {p₁ : α → γ} {p₂ : β → δ} {g : γ → δ} (comm : ∀ a, p₂ (f a) = g (p₁ a)) (hbij : BijOn f s t)
(hinj : InjOn g (p₁ '' s)) : BijOn g (p₁ '' s) (p₂ '' t) :=
by
obtain ⟨h1, h2, h3⟩ := hbij
refine ⟨?_, hinj, ?_⟩
· rintro _ ⟨a, ha, rfl⟩
exact ⟨f a, h1 ha, by rw [comm a]⟩
· rintro _ ⟨b, hb, rfl⟩
obtain ⟨a, ha, rfl⟩ := h3 hb
grind
