mem_bipartiteBelow

Mathlib.Combinatorics.Enumerative.DoubleCounting

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

English

An element a is in s.bipartiteBelow r b iff a ∈ s and r(a,b).

Русский

Элемент a принадлежит s.bipartiteBelow r b тогда и только тогда, когда a ∈ s и r(a,b).

LaTeX

$$$a \\in s.bipartiteBelow(r,b) \\iff a \\in s \\land r(a,b)$$$

Lean4

@[simp]
theorem mem_bipartiteBelow {a : α} : a ∈ s.bipartiteBelow r b ↔ a ∈ s ∧ r a b :=
  mem_filter

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

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

Разделы

Аффилиация

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