English
Given a function f that preserves addition and multiplication (a semiring homomorphism in the non-unital sense), IsQuasiregular x implies IsQuasiregular (f x).
Русский
Пусть f — гомоморфизм полупрямоугольника, сохраняющий сложение и умножение; тогда IsQuasiregular x следует из IsQuasiregular (f x).
LaTeX
$$$$ \text{IsQuasiregular}(x) \Rightarrow \text{IsQuasiregular}(f x) $$$$
Lean4
theorem map {F R S : Type*} [NonUnitalSemiring R] [NonUnitalSemiring S] [FunLike F R S] [NonUnitalRingHomClass F R S]
(f : F) {x : R} (hx : IsQuasiregular x) : IsQuasiregular (f x) :=
by
rw [isQuasiregular_iff] at hx ⊢
obtain ⟨y, hy₁, hy₂⟩ := hx
exact ⟨f y, by simpa using And.intro congr(f $(hy₁)) congr(f $(hy₂))⟩
