ext_iff — Mathlib

English

x ≡ y if and only if the left and right move components are equal as sets of moves.

Русский

x ≡ y тогда и только тогда, когда левая и правая составные части ходов равны как множества ходов.

LaTeX

$$$ x \equiv y \iff ( \forall z, z.mem_\ell x \leftrightarrow z.mem_\ell y) \land ( \forall z, z.mem_\mathrm{r} x \leftrightarrow z.mem_\mathrm{r} y)$$$

Lean4

theorem ext_iff {x y} : x ≡ y ↔ (∀ z, z ∈ₗ x ↔ z ∈ₗ y) ∧ (∀ z, z ∈ᵣ x ↔ z ∈ᵣ y) :=
  ⟨fun h ↦ ⟨@memₗ.congr_right _ _ h, @memᵣ.congr_right _ _ h⟩, fun h ↦ h.elim Identical.ext⟩

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