asymm_of

Mathlib.Order.Defs.Unbundled

URI: https://scilib.ai/kg/mathlib#asymm_of

English

If r is asymmetric, then a ≺ b → ¬ b ≺ a.

Русский

Если r асимметрично, то a ≺ b → ¬ b ≺ a.

LaTeX

$$$\forall a,b:\alpha, r a b \rightarrow \neg r b a$$$

Lean4

@[elab_without_expected_type]
theorem asymm_of [IsAsymm α r] : a ≺ b → ¬b ≺ a :=
  asymm

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

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

Разделы

Аффилиация

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