Iic_one

Mathlib.Algebra.Order.UpperLower

URI: https://scilib.ai/kg/mathlib#LowerSet.Iic_one

English

There is a MulAction α (LowerSet α) with action a • S = image under a acting on S.

Русский

Существует MulAction α (LowerSet α) с действием a • S = образ при действии a над S.

LaTeX

$$There exists a MulAction α (LowerSet α) defined by a • S = { a x : x ∈ S }$$

Lean4

@[to_additive (attr := simp)]
theorem Iic_one : Iic (1 : α) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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