pointwise_smul_subset_iff — Mathlib

English

For a ∈ α and Submonoids S, T of M, S ≤ a⁻¹ · T iff S ≤ a⁻¹ · T in the opposite sense (duality form).

Русский

Для a ∈ α и подмономов S, T в M: S ≤ a⁻¹ · T эквивалентно соответствующему двойственному условию.

LaTeX

$$$S \\le a^{-1} \\cdot T \\;\\text{ iff }\\; a \\cdot S \\le T$$$

Lean4

theorem pointwise_smul_subset_iff {a : α} {S T : Submonoid M} : a • S ≤ T ↔ S ≤ a⁻¹ • T :=
  smul_set_subset_iff_subset_inv_smul_set

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