instIsAsymm

Mathlib.Order.RelClasses

URI: https://scilib.ai/kg/mathlib#Order.Preimage.instIsAsymm

English

If r is asymmetric on α, then the preimage order on β is asymmetric.

Русский

Если $r$ ассиметрично на $\alpha$, то $f^{-1'o r}$ ассиметрично на $\beta$.

LaTeX

$$IsAsymm(β, (f⁻¹'o r))$$

Lean4

instance instIsAsymm [IsAsymm α r] {f : β → α} : IsAsymm β (f ⁻¹'o r) :=
  ⟨fun _ _ ↦ asymm_of r⟩

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

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

Разделы

Аффилиация

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