inv_subset_inv

Mathlib.Algebra.Group.Pointwise.Set.Basic

URI: https://scilib.ai/kg/mathlib#Set.inv_subset_inv

English

Inversion reverses inclusion: s^{-1} ⊆ t^{-1} if and only if s ⊆ t.

Русский

Инверсия обращает включение: s^{-1} ⊆ t^{-1} эквивалентно s ⊆ t.

LaTeX

$$$ s^{-1} \subseteq t^{-1} \iff s \subseteq t $$$

Lean4

@[to_additive (attr := simp)]
theorem inv_subset_inv : s⁻¹ ⊆ t⁻¹ ↔ s ⊆ t :=
  (Equiv.inv α).surjective.preimage_subset_preimage_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru