pi_congr

Mathlib.Data.Set.Prod

URI: https://scilib.ai/kg/mathlib#Set.pi_congr

English

If s₁ = s₂ and t₁ i = t₂ i for all i ∈ s₁, then s₁.pi t₁ = s₂.pi t₂.

Русский

Если s₁ = s₂ и для всех i ∈ s₁ выполняется t₁ i = t₂ i, то s₁.pi t₁ = s₂.pi t₂.

LaTeX

$$$ s₁ = s₂ \Rightarrow (\forall i \in s₁, t₁ i = t₂ i) \Rightarrow s₁.pi t₁ = s₂.pi t₂ $$$

Lean4

theorem pi_congr (h : s₁ = s₂) (h' : ∀ i ∈ s₁, t₁ i = t₂ i) : s₁.pi t₁ = s₂.pi t₂ := by grind

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru