coe_bipartiteBelow

Mathlib.Combinatorics.Enumerative.DoubleCounting

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

English

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

Русский

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

LaTeX

$$$t.bipartiteBelow(r,b) = \\{a \\in s \\mid r(a,b)\\}\\;: \\text{Set} \\;\\alpha$$$

Lean4

@[simp, norm_cast]
theorem coe_bipartiteBelow : s.bipartiteBelow r b = ({a ∈ s | r a b} : Set α) :=
  coe_filter _ _

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

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

Разделы

Аффилиация

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