le_of_le_graph — Mathlib

English

If the graph of f is contained in the graph of g, then f is less than or equal to g in the natural order on linear partial maps.

Русский

Если график f содержится в графике g, то f слева от g в естественном порядке линейных частичных отображений.

LaTeX

$$$ f.graph \\le g.graph \\Rightarrow f \\le g $$$

Lean4

theorem le_of_le_graph {f g : E →ₗ.[R] F} (h : f.graph ≤ g.graph) : f ≤ g :=
  by
  constructor
  · intro x hx
    rw [mem_domain_iff] at hx ⊢
    obtain ⟨y, hx⟩ := hx
    use y
    exact h hx
  rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
  rw [image_iff]
  refine h ?_
  simp only at hxy
  rw [hxy] at hx
  rw [← image_iff hx]
  simp [hxy]

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