union_C0C1_eq

Mathlib.Topology.Category.Profinite.Nobeling.Successor

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.union_C0C1_eq

← MathLib Explorer

English

The union of C0 and C1 equals C.

Русский

Объединение C0 и C1 даёт C.

LaTeX

$$ (C0 C ho) ∪ (C1 C ho) = C $$

Lean4

theorem union_C0C1_eq : (C0 C ho) ∪ (C1 C ho) = C := by
  ext x
  simp only [C0, C1, Set.mem_union, Set.mem_inter_iff, Set.mem_setOf_eq, ← and_or_left, and_iff_left_iff_imp,
    Bool.dichotomy (x (term I ho)), implies_true]

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

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

Разделы

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

Аффилиация

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