coe_le_coe

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#NonarchAddGroupNorm.coe_le_coe

English

Iff between the pointwise Le on functions and the NonarchAddGroupNorm order: (p ≤ q) ⇔ (p as function) ≤ (q as function).

Русский

Эквивалентность между поэлементным ≤ и порядком NonarchAddGroupNorm: p ≤ q ⇔ (p как функция) ≤ (q как функция).

LaTeX

$$p ≤ q iff (p: E→ℝ) ≤ q$$

Lean4

@[simp, norm_cast]
theorem coe_le_coe : (p : E → ℝ) ≤ q ↔ p ≤ q :=
  Iff.rfl

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

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

Разделы

Аффилиация

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