fst_eq_iff

Mathlib.Data.Prod.Basic

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

English

For p ∈ α × β and x ∈ α, p.fst = x iff p = (x, p.snd).

Русский

Для p ∈ α × β и x ∈ α, p.fst = x эквивалентно p = (x, p.snd).

LaTeX

$$$\\\\forall {p : \\\\alpha \\\\times \\\\beta} {x : \\\\alpha}, p.1 = x \\\\iff p = (x, p.2)$$$

Lean4

theorem fst_eq_iff : ∀ {p : α × β} {x : α}, p.1 = x ↔ p = (x, p.2)
  | ⟨a, b⟩, x => by simp

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

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

Разделы

Аффилиация

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