mem_single_iff — Mathlib

English

The element b1 belongs to the image single a2 b2 a1 exactly when a1 = a2 and b1 = b2.

Русский

Элемент b1 принадлежит множеству, полученному через single a2 b2 a1, тогда и только тогда a1 = a2 и b1 = b2.

LaTeX

$$$b_1 \in single a_2 b_2 a_1 \iff a_1 = a_2 \land b_1 = b_2$$$

Lean4

theorem mem_single_iff (a₁ a₂ : α) (b₁ b₂ : β) : b₁ ∈ single a₂ b₂ a₁ ↔ a₁ = a₂ ∧ b₁ = b₂ := by dsimp [single];
  split_ifs <;> simp [*, eq_comm]

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