self_mem_codiscreteWithin

Mathlib.Topology.DiscreteSubset

URI: https://scilib.ai/kg/mathlib#Filter.self_mem_codiscreteWithin

← MathLib Explorer

English

Every set is trivially a member of codiscreteWithin within itself.

Русский

Каждое множество является членом codiscreteWithin внутри самого себя.

LaTeX

$$$\\text{self\_mem\_codiscreteWithin}(U): U \\in \\operatorname{codiscreteWithin}(U)$$$

Lean4

/-- Any set is codiscrete within itself. -/
@[simp]
theorem self_mem_codiscreteWithin (U : Set X) : U ∈ Filter.codiscreteWithin U := by simp [mem_codiscreteWithin]

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

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

Разделы

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

Аффилиация

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