instDecidablePredShatters

Mathlib.Combinatorics.SetFamily.Shatter

URI: https://scilib.ai/kg/mathlib#Finset.instDecidablePredShatters

English

There exists a decidable instance for the predicate 𝒜.Shatters.

Русский

Существует решаемый экземпляр предиката 𝒜.Shatters.

LaTeX

$$$\operatorname{DecidablePred}( 𝒜.\mathrm{Shatters} )$$$

Lean4

instance : DecidablePred 𝒜.Shatters := fun _s ↦ decidableForallOfDecidableSubsets

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

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

Разделы

Аффилиация

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