symmetric_apply_eq_iff — Mathlib

English

The relation x ∼ y defined by f x = y is symmetric iff f is involutive.

Русский

Отношение x ∼ y, заданное f x = y, симметрично тогда и только тогда, когда f инволютивна.

LaTeX

$$$ \\forall {f : \\alpha \\to \\alpha}, \\operatorname{Symmetric}(f\\,\\cdot = \\cdot) \\iff \\operatorname{Involutive} f $$$

Lean4

@[simp]
theorem symmetric_apply_eq_iff {α : Sort*} {f : α → α} : Symmetric (f · = ·) ↔ Involutive f := by
  simp [Symmetric, Involutive]

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