blur_eq_blur'

Mathlib.Data.Semiquot

URI: https://scilib.ai/kg/mathlib#Semiquot.blur_eq_blur'

← MathLib Explorer

English

If h holds (q.s ⊆ s), then blur s q equals blur' q h.

Русский

Если выполняется условие h (q.s ⊆ s), то blur s q = blur' q h.

LaTeX

$$$blur\ s\ q = blur'\ q\ h$$$

Lean4

theorem blur_eq_blur' (q : Semiquot α) (s : Set α) (h : q.s ⊆ s) : blur s q = blur' q h := by unfold blur; congr;
  exact Set.union_eq_self_of_subset_right h

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

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

Разделы

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

Аффилиация

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