inv_pi — Mathlib

English

Given a family of sets t(i) in α(i) and a subset s of the index set, the inverse of the pi-set equals the pi-set of inverses: (s.pi t)⁻¹ = s.pi (i ↦ t(i)⁻¹).

Русский

Пусть имеется семейство множеств t(i) ⊆ α(i) и подмножество индексов s. Тогда инверсия пи-множества действует по координатам: (s.pi t)⁻¹ = s.pi (i ↦ t(i)⁻¹).

LaTeX

$$(s \\ pi t)^{-1} = s \\ pi (i \\mapsto (t(i))^{-1})$$

Lean4

@[to_additive (attr := simp)]
theorem inv_pi (s : Set ι) (t : ∀ i, Set (α i)) : (s.pi t)⁻¹ = s.pi fun i ↦ (t i)⁻¹ := by ext x; simp

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