le_op_iff

Mathlib.Algebra.Group.Submonoid.MulOpposite

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

English

A duality re: inclusion for op and unop: S1 ≤ S2.op iff S1.unop ≤ S2.

Русский

Двойственность включений между S1 и S2 через op и unop: S1 ≤ S2.op эквивалентно S1.unop ≤ S2.

LaTeX

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

Lean4

@[to_additive]
theorem le_op_iff {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M} : S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂ :=
  MulOpposite.op_surjective.forall

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

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

Разделы

Аффилиация

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