unop_le_unop_iff

Mathlib.Algebra.Group.Submonoid.MulOpposite

URI: https://scilib.ai/kg/mathlib#Submonoid.unop_le_unop_iff

English

For S1,S2 in Mᵐᵒᵖ, S1.unop ≤ S2.unop iff S1 ≤ S2.

Русский

Для S1,S2 в Mᵐᵒᵖ: S1.unop ≤ S2.unop эквивалентно S1 ≤ S2.

LaTeX

$$$S_1^{unop} \le S_2^{unop} \iff S_1 \le S_2$.$$

Lean4

@[to_additive (attr := simp)]
theorem unop_le_unop_iff {S₁ S₂ : Submonoid Mᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
  MulOpposite.unop_surjective.forall

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

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

Разделы

Аффилиация

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