le_def

Mathlib.Topology.ContinuousMap.CompactlySupported

URI: https://scilib.ai/kg/mathlib#CompactlySupportedContinuousMap.le_def

English

The strict order on C_c(α,β) is characterized by: f < g iff f ≤ g for all a and there exists some a with f(a) < g(a).

Русский

Строгое неравенство: f < g тогда и только тогда, когда f ≤ g для всех a и существует a с f(a) < g(a).

LaTeX

$$$f < g \iff (\forall a, f(a) \le g(a)) \land \exists a, f(a) < g(a)$$$

Lean4

theorem le_def {f g : C_c(α, β)} : f ≤ g ↔ ∀ a, f a ≤ g a :=
  Pi.le_def

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru