mem_blur'

Mathlib.Data.Semiquot

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

English

Membership in blur' q h is exactly membership in s.

Русский

Членство в blur' q h эквивалентно членству в s.

LaTeX

$$$a \in blur' q h \iff a \in s$$$

Lean4

@[simp]
theorem mem_blur' (q : Semiquot α) {s : Set α} (h : q.s ⊆ s) {a : α} : a ∈ blur' q h ↔ a ∈ s :=
  Iff.rfl

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

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

Разделы

Аффилиация

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