le_def — Mathlib

English

For continuous maps f,g: α → β, f ≤ g if and only if for every a ∈ α one has f(a) ≤ g(a).

Русский

Для непрерывных отображений f,g: α → β верно: f ≤ g тогда и только тогда, когда для каждой точки a выполняется f(a) ≤ g(a).

LaTeX

$$\$f, g : C(α, β)\$ — f ≤ g если и только если ∀ a, f(a) ≤ g(a).$$

Lean4

theorem le_def [PartialOrder β] {f g : C(α, β)} : f ≤ g ↔ ∀ a, f a ≤ g a :=
  Pi.le_def

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