map — Mathlib

English

If f is surjective, then every square in the codomain is the image under f of a square in the domain.

Русский

Пусть f сюръективно отображает, тогда каждый квадрат в кодомапе является образом квадрата из области.

LaTeX

$$$\{b \mid \operatorname{IsSquare}(b)\} \subseteq f '' \{a \mid \operatorname{IsSquare}(a)\}$$$

Lean4

@[to_additive (attr := aesop unsafe 90%)]
theorem map {a : α} (f : F) : IsSquare a → IsSquare (f a) := fun ⟨r, _⟩ => ⟨f r, by simp [*]⟩

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