gc_count_nth

Mathlib.Data.Nat.Nth

URI: https://scilib.ai/kg/mathlib#Nat.gc_count_nth

English

Theorem: For predicate p, there is a Galois connection between count p and nth p; i.e., count p and nth p are related by a Galois correspondence.

Русский

Существует Галуа-коотношение между count p и nth p.

LaTeX

$$$$ \\text{Galois connection between } \\mathrm{count}(p) \\text{ and } \\mathrm{nth}(p). $$$$

Lean4

theorem gc_count_nth (hp : (setOf p).Infinite) : GaloisConnection (count p) (nth p) :=
  (giCountNth hp).gc

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

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

Разделы

Аффилиация

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