covBy_iff_wcovBy_and_ne

Mathlib.Order.Cover

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

English

A is covered by B if and only if A is weakly covered by B and A ≠ B.

Русский

A ⋖ B эквивалентно A ⩿ B и A ≠ B.

LaTeX

$$$ a ⋖ b \\iff a ⩿ b \\land a \\ne b $$$

Lean4

theorem covBy_iff_wcovBy_and_ne : a ⋖ b ↔ a ⩿ b ∧ a ≠ b :=
  ⟨fun h => ⟨h.wcovBy, h.ne⟩, fun h => h.1.covBy_of_ne h.2⟩

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

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

Разделы

Аффилиация

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