piSetoid

Mathlib.Data.Quot

URI: https://scilib.ai/kg/mathlib#piSetoid

Lean4

instance piSetoid {ι : Sort*} {α : ι → Sort*} [∀ i, Setoid (α i)] : Setoid (∀ i, α i)
    where
  r a b := ∀ i, a i ≈ b i
  iseqv := ⟨fun _ _ ↦ Setoid.refl _, fun h _ ↦ Setoid.symm (h _), fun h₁ h₂ _ ↦ Setoid.trans (h₁ _) (h₂ _)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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