mem_falling

Mathlib.Combinatorics.SetFamily.LYM

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

English

A simplified form of exists_mem_set specialized to falling sets.

Русский

Упрощенная форма существования общего элемента для падения множеств.

LaTeX

$$$\exists a \; a \in s \land a \in t$$$

Lean4

theorem mem_falling : s ∈ falling k 𝒜 ↔ (∃ t ∈ 𝒜, s ⊆ t) ∧ #s = k :=
  by
  simp_rw [falling, mem_sup, mem_powersetCard]
  aesop

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

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

Разделы

Аффилиация

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