English
The map f is surjective between α and β iff FreeMonoid.map f is surjective on FreeMonoid β; i.e., map_surjective ↔ surjectivity of f.
Русский
Функция f сюръективна тогда и только тогда, когда отображение FreeMonoid.map f сюръективно на FreeMonoid β.
LaTeX
$$$ \text{Surjective}(\ map\ f) \iff \text{Surjective}(f) $$$
Lean4
@[to_additive (attr := simp)]
theorem map_surjective {f : α → β} : Function.Surjective (map f) ↔ Function.Surjective f :=
by
constructor
· intro fs d
rcases fs (FreeMonoid.of d) with ⟨b, hb⟩
induction b using FreeMonoid.inductionOn' with
| one =>
have H := congr_arg length hb
simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
| mul_of head _ _ =>
simp only [map_mul, map_of] at hb
use head
have H := congr_arg length hb
simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
rw [H, mul_one] at hb
exact FreeMonoid.of_injective hb
intro fs d
induction d using FreeMonoid.inductionOn' with
| one => use 1; rfl
| mul_of head tail ih =>
specialize fs head
rcases fs with ⟨a, rfl⟩
rcases ih with ⟨b, rfl⟩
use FreeMonoid.of a * b
rfl
