ofRel — Mathlib

English

For any binary relation r on α, the ideal generated by r is the smallest ideal containing all differences a − b for which r(a,b) holds.

Русский

Для любой двоичной связи r на α идеал, порожденный r, есть наименьший идеал, содержащий все разности a − b, для которых r(a,b) выполняется.

LaTeX

$$$$ \operatorname{span}_{\alpha} \{ x \mid \exists a,b,\ r(a,b) \land x + b = a \} $$$$

Lean4

/-- The ideal generated by an arbitrary binary relation. -/
def ofRel (r : α → α → Prop) : Ideal α :=
  Submodule.span α {x | ∃ a b, r a b ∧ x + b = a}

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