blur

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.blur

← MathLib Explorer

English

Replace s in q by the union s ∪ q.s to obtain a new Semiquot.

Русский

Заменяемое множество оснований в q на объединение s ∪ q.s для получения нового семикуота.

LaTeX

$$$(blur\ s\ q).s = s \cup q.s$$$

Lean4

/-- Replace `s` in a `q : Semiquot α` with a union `s ∪ q.s` -/
def blur (s : Set α) (q : Semiquot α) : Semiquot α :=
  blur' q (s.subset_union_right (t := q.s))

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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