sigma_subset_iff — Mathlib

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

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