specializes_pi — Mathlib

English

For functions f,g from a index set to A_i, f ⤳ g iff ∀ i, f(i) ⤳ g(i).

Русский

Для функций f,g из индекса в множества A_i, f ⤳ g тогда и только тогда, когда для всех i выполняется f(i) ⤳ g(i).

LaTeX

$$$$ f \rightsquigarrow g \iff \forall i, f(i) \rightsquigarrow g(i). $$$$

Lean4

@[simp]
theorem specializes_pi {f g : ∀ i, A i} : f ⤳ g ↔ ∀ i, f i ⤳ g i := by simp only [Specializes, nhds_pi, pi_le_pi]

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