subset_pi_iff — Mathlib

English

A subset s' is contained in the dependent product pi s t if and only if for every i in s, s' is contained in the preimage under the i-th projection of t_i.

Русский

Подмножество s' содержится в произведении pi s t тогда и только тогда, когда для каждого i ∈ s выполняется s' ⊆ (· i)^{-1} t_i.

LaTeX

$$$$ s' \\subseteq \\pi s t \\quad\\Longleftrightarrow\\quad \\forall i \\in s,\\ s' \\subseteq (\\cdot i)^{-1} t_i. $$$$

Lean4

theorem subset_pi_iff {s'} : s' ⊆ pi s t ↔ ∀ i ∈ s, s' ⊆ (· i) ⁻¹' t i := by grind

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