full_mono — Mathlib

English

If D ⊆ E, then the full subgroupoid on D is contained in the full subgroupoid on E.

Русский

Если D ⊆ E, то полная подгруппоида на D содержится в полной подгруппоида на E.

LaTeX

$$$\\forall D E \\subseteq C,\\ D \\le E \\Rightarrow full\\ D \\le full\\ E$$$

Lean4

theorem full_mono {D E : Set C} (h : D ≤ E) : full D ≤ full E :=
  by
  rw [le_iff]
  rintro c d f
  simp only [mem_full_iff]
  exact fun ⟨hc, hd⟩ => ⟨h hc, h hd⟩

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