English
A sigma subset relation is equivalent to pointwise membership: s.sigma t ⊆ u iff for all i ∈ s and a ∈ t i, ⟨i,a⟩ ∈ u.
Русский
Отношение подмножества сигма эквивалентно по координатам: s.sigma t ⊆ u тогда и только тогда, когда для всех i∈s и a∈t i верно ⟨i,a⟩ ∈ u.
LaTeX
$$$s.\\sigma t \\subseteq u \\iff \\forall i \\in s, \\forall a \\in t(i), (\\langle i,a\\rangle) \\in u$$$
Lean4
theorem sigma_subset_iff : s.sigma t ⊆ u ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃a⦄, a ∈ t i → (⟨i, a⟩ : Σ i, α i) ∈ u := by grind