mem_C'_eq_false

Mathlib.Topology.Category.Profinite.Nobeling.Successor

URI: https://scilib.ai/kg/mathlib#Profinite.NobelingProof.mem_C'_eq_false

← MathLib Explorer

English

As above, elements of C' evaluate to false at the distinguished term.

Русский

Элементы C' должны давать false в заданной точке.

LaTeX

$$$\\forall x:\\I,\\ x \\in C' C ho \\Rightarrow x(\\mathrm{term}\\ I ho) = \\mathrm{false}$$$

Lean4

theorem mem_C'_eq_false : ∀ x, x ∈ C' C ho → x (term I ho) = false :=
  by
  rintro x ⟨_, y, _, rfl⟩
  simp only [Proj, ord_term_aux, lt_self_iff_false, ite_false]

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

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

Разделы

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

Аффилиация

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