le_graph_of_le — Mathlib

English

If f ≤ g, then the graph of f is contained in the graph of g.

Русский

Если f ≤ g, то график f содержится в графике g.

LaTeX

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

Lean4

theorem le_graph_of_le {f g : E →ₗ.[R] F} (h : f ≤ g) : f.graph ≤ g.graph :=
  by
  intro x hx
  rw [mem_graph_iff] at hx ⊢
  obtain ⟨y, hx⟩ := hx
  use ⟨y, h.1 y.2⟩
  simp only [hx, true_and]
  convert hx.2 using 1
  refine (h.2 ?_).symm
  simp only [hx.1]

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