coe_lt_coe

Mathlib.Analysis.Normed.Group.Seminorm

URI: https://scilib.ai/kg/mathlib#NonarchAddGroupSeminorm.coe_lt_coe

English

For p, q ∈ NonarchAddGroupSeminorm E, (p : E → ℝ) < q if and only if p < q.

Русский

Для p, q ∈ NonarchAddGroupSeminorm E, (p : E → ℝ) < q тогда и только тогда, когда p < q.

LaTeX

$$$ (p : E \to \mathbb{R}) < q \iff p < q $$$

Lean4

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

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

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

Разделы

Аффилиация

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