contained_proj

Mathlib.Topology.Category.Profinite.Nobeling.Basic

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

English

The predicate contained is closed under the π-projections in Nobeling framework.

Русский

Предикат contained сохраняется под проекциями π в рамках Нобелинг-подстановки.

LaTeX

$$$\\text{contained}(C)\\Rightarrow \\text{...}$$$

Lean4

theorem contained_proj (o : Ordinal) : contained (π C (ord I · < o)) o :=
  by
  intro x ⟨_, _, h⟩ j hj
  aesop (add simp Proj)

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

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

Разделы

Аффилиация

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