empty_mem_iff

Mathlib.Data.Finset.Slice

URI: https://scilib.ai/kg/mathlib#Set.Sized.empty_mem_iff

English

For A.Sized r, the empty Finset ∅ belongs to A if and only if A = {∅}.

Русский

Для A.Sized r верно: ∅ ∈ A тогда и только тогда, когда A = {∅}.

LaTeX

$$$\\text{If } A.Sized(r)\\text{ then } ∅ \\in A \\iff A = \\{∅\\}. $$$

Lean4

theorem empty_mem_iff (hA : A.Sized r) : ∅ ∈ A ↔ A = {∅} :=
  hA.isAntichain.bot_mem_iff

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

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

Разделы

Аффилиация

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