Sized

Mathlib.Data.Finset.Slice

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

English

Sized r A means every finite set in A has cardinality r.

Русский

Sized r A означает, что каждая конечная подмножество в A имеет кардинальность r.

LaTeX

$$$$ \mathrm{Sized}(r,A) := \forall x\ (x \in A \rightarrow |x| = r) $$$$

Lean4

/-- `Sized r A` means that every Finset in `A` has size `r`. -/
def Sized (r : ℕ) (A : Set (Finset α)) : Prop :=
  ∀ ⦃x⦄, x ∈ A → #x = r

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

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

Разделы

Аффилиация

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