iff

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Symmetric.iff

English

If r is symmetric, then r x y ⇔ r y x for all x,y.

Русский

Если r симметрично, то для любых x,y выполняется r x y ⇔ r y x.

LaTeX

$$$\\operatorname{Symmetric}(r) \\Rightarrow \\forall x,y,\\ r x y \\iff r y x$$$

Lean4

protected theorem iff (H : Symmetric r) (x y : α) : r x y ↔ r y x :=
  ⟨fun h ↦ H h, fun h ↦ H h⟩

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

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

Разделы

Аффилиация

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