isEmpty_false

Mathlib.Logic.IsEmpty

URI: https://scilib.ai/kg/mathlib#Subtype.isEmpty_false

English

Subtypes by false predicate are empty.

Русский

Подтипы по ложному предикату пусты.

LaTeX

$$$ [IsEmpty(α)] IsEmpty(Subtype(\lambda x, False)) $$$

Lean4

/-- subtypes by false are false. -/
instance isEmpty_false : IsEmpty { _a : α // False } :=
  Subtype.isEmpty_of_false fun _ ↦ id

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

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

Разделы

Аффилиация

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