eq_iff_fst_eq_snd_eq

Mathlib.Data.Prod.Basic

URI: https://scilib.ai/kg/mathlib#Prod.eq_iff_fst_eq_snd_eq

English

For p,q ∈ α × β, p = q iff p.fst = q.fst and p.snd = q.snd.

Русский

Для p,q ∈ α × β, p = q, если и только если p.fst = q.fst и p.snd = q.snd.

LaTeX

$$$\\\\forall p,q \\\\in \\\\alpha \\\\times \\\\beta, \\\\operatorname{Eq}(p,q) \\\\\\iff \\\\operatorname{And}(p.1 = q.1, p.2 = q.2).$$$

Lean4

theorem eq_iff_fst_eq_snd_eq : ∀ {p q : α × β}, p = q ↔ p.1 = q.1 ∧ p.2 = q.2
  | ⟨p₁, p₂⟩, ⟨q₁, q₂⟩ => by simp

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

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

Разделы

Аффилиация

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