contains — Mathlib

English

If a fractional operation is valid, it contains at least one function g in the multiset.

Русский

Для допустимой фракционной операции существует элемент g, принадлежащий мультисету.

LaTeX

$$$\\exists g\\in ω, g:(Fin m \\to D)\\to D$$$

Lean4

/-- Valid fractional operation contains an operation. -/
theorem contains {ω : FractionalOperation D m} (valid : ω.IsValid) : ∃ g : (Fin m → D) → D, g ∈ ω :=
  Multiset.exists_mem_of_ne_zero valid

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