apply_covBy_apply_iff — Mathlib

English

For partial orders, the covBy relation is preserved along an initial segment embedding.

Русский

Для частичных порядков отношение covBy сохраняется через отображение начального сегмента.

LaTeX

$$$ f a \\covBy f b \\iff a \\covBy b $$$

Lean4

@[simp]
theorem apply_covBy_apply_iff (f : α ≤i β) : f a ⋖ f b ↔ a ⋖ b :=
  (isLowerSet_range f).ordConnected.apply_covBy_apply_iff f.toOrderEmbedding

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