pointwise_smul_subset_iff — Mathlib

English

Let g ∈ G and S, T be valuation subrings of K. Then g · S ⊆ T iff S ⊆ g⁻¹ · T.

Русский

Пусть g ∈ G и S, T — valuation subrings из K. Тогда g · S ⊆ T эквивалентно S ⊆ g⁻¹ · T.

LaTeX

$$$\\\\forall g \in G, \\\\forall S,T \\\\text{ ValuationSubring}(K):\\\\ g \\\\cdot S \subseteq T \iff S \subseteq g^{-1} \\\\cdot T.$$$

Lean4

theorem pointwise_smul_subset_iff {g : G} {S T : ValuationSubring K} : g • S ≤ T ↔ S ≤ g⁻¹ • T :=
  Set.smul_set_subset_iff_subset_inv_smul_set

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