mem_iSup — Mathlib

English

Membership in the supremum (iSup) of a family of languages is equivalent to belonging to some member of the family.

Русский

Членство в верхней оболочке (iSup) семейства языков эквивалентно принадлежности какому-либо языку из семейства.

LaTeX

$$$ (x \in \bigsqcup_i l_i) \iff \exists i, x \in l_i $$$

Lean4

theorem mem_iSup {ι : Sort v} {l : ι → Language α} {x : List α} : (x ∈ ⨆ i, l i) ↔ ∃ i, x ∈ l i :=
  mem_iUnion

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