mem_bipartiteAbove

Mathlib.Combinatorics.Enumerative.DoubleCounting

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

English

An element b is in t.bipartiteAbove r a iff b ∈ t and r(a,b).

Русский

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

LaTeX

$$$b \\in t.bipartiteAbove(r,a) \\iff b \\in t \\land r(a,b)$$$

Lean4

@[simp]
theorem mem_bipartiteAbove {b : β} : b ∈ t.bipartiteAbove r a ↔ b ∈ t ∧ r a b :=
  mem_filter

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

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

Разделы

Аффилиация

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