instDiv

Mathlib.Algebra.Order.UpperLower

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

English

For any a ∈ α and S ∈ LowerSet α, the smul a • S is the lower set { a x | x ∈ S }.

Русский

Для любого a ∈ α и S ∈ LowerSet α, действие смул: a • S = { a x | x ∈ S }.

LaTeX

$$a ∈ α, S ∈ \\text{LowerSet}(α) ⇒ a \\cdot S = \\{ a x : x ∈ S \\}$$

Lean4

@[to_additive]
instance : Div (LowerSet α) :=
  ⟨fun s t ↦ ⟨image2 (· / ·) s t, s.2.div_right⟩⟩

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

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

Разделы

Аффилиация

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