isSquare_subset_image_isSquare — Mathlib

English

If f is surjective, then the set of squares in the codomain is contained in the image under f of the squares in the domain.

Русский

Если f сюръективно отображает, то множество квадратов в кодомапе содержится в образе квадратов из области.

LaTeX

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

Lean4

@[to_additive]
theorem isSquare_subset_image_isSquare {f : F} (hf : Function.Surjective f) :
    {b | IsSquare b} ⊆ f '' {a | IsSquare a} := fun b ⟨s, _⟩ =>
  by
  rcases hf s with ⟨r, rfl⟩
  exact ⟨r * r, by simp [*]⟩

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