MaxProducts — Mathlib

English

MaxProducts is the set of those products in I for which the product has the Good property with respect to C and contains the distinguished term.

Русский

MaxProducts — множество изделий в I, удовлетворяющих свойству Good относительно C и содержащих особый член.

LaTeX

$$$\\operatorname{MaxProducts} C ho = \\{ l:\\ Profinite.NobelingProof.Products I \\mid l.isGood C \\land \\operatorname{term} I ho \\in l.val \\}$$$

Lean4

/-- The `GoodProducts` in `C` that contain `o` (they necessarily start with `o`, see
`GoodProducts.head!_eq_o_of_maxProducts`)
-/
def MaxProducts : Set (Products I) :=
  {l | l.isGood C ∧ term I ho ∈ l.val}

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