coe_bipartiteAbove

Mathlib.Combinatorics.Enumerative.DoubleCounting

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

English

The finite-set bipartiteAbove corresponds to the set {b ∈ t | r a b} under coercion to a Set.

Русский

mножество bipartiteAbove конвертируется в множество {b ∈ t | r a b}.

LaTeX

$$$t.bipartiteAbove(r,a) = \\{b \\in t \\mid r(a,b)\\}\\;: \\text{Set} \\;\\beta$$$

Lean4

@[simp, norm_cast]
theorem coe_bipartiteAbove : t.bipartiteAbove r a = ({b ∈ t | r a b} : Set β) :=
  coe_filter _ _

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

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

Разделы

Аффилиация

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