apply_covBy_apply_iff — Mathlib

English

If f is an order-embedding mapping, then f a is covered by f b iff a is covered by b; i.e., the cover relation is preserved by f.

Русский

Если f — отображение, сохраняющее порядок, то f a покрывает f b тогда и только тогда, когда a покрывает b; т. е. отношение покрытия сохраняется под f.

LaTeX

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

Lean4

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

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