apply_wCovBy_apply_iff

Mathlib.Order.SuccPred.InitialSeg

URI: https://scilib.ai/kg/mathlib#PrincipalSeg.apply_wCovBy_apply_iff

English

For a weak cover relation, applying the embedding preserves the weak cover relation: f a ⩿ f b iff a ⩿ b.

Русский

Для слабого отношения покрытия сохранение сохраняется: f a ⩿ f b ⇔ a ⩿ b.

LaTeX

$$$f(a) \trianglelefteq f(b) \iff a \trianglelefteq b$$$

Lean4

@[simp]
theorem apply_wCovBy_apply_iff (f : α <i β) : f a ⩿ f b ↔ a ⩿ b :=
  (f : α ≤i β).apply_wCovBy_apply_iff

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

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

Разделы

Аффилиация

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