coe_mono — Mathlib

English

Let f,g be dependent finite-support functions with f ≤ g. Then the pointwise values satisfy f(i) ≤ g(i) for every i; equivalently, the embedding is order-preserving.

Русский

Пусть f,g — функции с конечной опорой; если f ≤ g, то f(i) ≤ g(i) для каждого i; иначе говоря, отображение сохраняет порядок.

LaTeX

$$$$ f \le g \implies (\forall i, f(i) \le g(i)). $$$$

Lean4

theorem coe_mono : Monotone ((⇑) : (Π₀ i, α i) → ∀ i, α i) := fun _ _ ↦ id

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