val_covBy_val

Mathlib.Data.Finset.Grade

URI: https://scilib.ai/kg/mathlib#Finset.val_covBy_val

English

Two Finsets are in CovBy relation precisely when their underlying multisets are in CovBy relation.

Русский

Два Finset лежат в отношении CovBy тогда, когда их базовые мультсет-образы находятся в CovBy.

LaTeX

$$$ s.1 \covBy t.1 \iff s \covBy t $$$

Lean4

@[simp]
theorem val_covBy_val : s.1 ⋖ t.1 ↔ s ⋖ t :=
  ordConnected_range_val.apply_covBy_apply_iff ⟨⟨_, val_injective⟩, val_le_iff⟩

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

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

Разделы

Аффилиация

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