exists_of_le

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.exists_of_le

English

If f ≤ g and their domains are equal, then f = g.

Русский

Если f ≤ g и их области определения совпадают, то f = g.

LaTeX

$$$\text{LinearPMap}.eq_of_le_of_domain_eq\ hle\ hdom : f ≤ g \land f.domain = g.domain \Rightarrow f = g$$$

Lean4

theorem exists_of_le {T S : E →ₗ.[R] F} (h : T ≤ S) (x : T.domain) : ∃ y : S.domain, (x : E) = y ∧ T x = S y :=
  ⟨⟨x.1, h.1 x.2⟩, ⟨rfl, h.2 rfl⟩⟩

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

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

Разделы

Аффилиация

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