subset_smul_set_iff — Mathlib

English

For A,B ⊆ β and a ∈ α, A ⊆ a • B is equivalent to a⁻¹ • A ⊆ B.

Русский

Для A,B ⊆ β и a ∈ α: A ⊆ a•B эквивалентно a⁻¹•A ⊆ B.

LaTeX

$$$A\subseteq a\cdot B \iff a^{-1}\cdot A\subseteq B.$$$

Lean4

@[to_additive]
theorem subset_smul_set_iff : A ⊆ a • B ↔ a⁻¹ • A ⊆ B :=
  Iff.symm <|
    image_subset_iff.trans <|
      Iff.symm <| iff_of_eq <| congr_arg _ <| image_equiv_eq_preimage_symm _ <| MulAction.toPerm _

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