mono — Mathlib

English

If K ≤ L then IsApproximateSubgroup K A implies IsApproximateSubgroup L A.

Русский

Если K ≤ L, то из IsApproximateSubgroup K A следует IsApproximateSubgroup L A.

LaTeX

$$$(K \\le L) \\Rightarrow (\\IsApproximateSubgroup K A) \\Rightarrow (\\IsApproximateSubgroup L A)$$$

Lean4

@[to_additive]
theorem mono (hKL : K ≤ L) (hA : IsApproximateSubgroup K A) : IsApproximateSubgroup L A
    where
  one_mem := hA.one_mem
  inv_eq_self := hA.inv_eq_self
  sq_covBySMul := hA.sq_covBySMul.mono hKL

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