range_inclusion — Mathlib

English

If s ⊆ t, then range (inclusion s→t) equals { x ∈ t | (x : α) ∈ s }.

Русский

Если s ⊆ t, то range (inclusion s→t) совпадает с { x ∈ t | (x : α) ∈ s }.

LaTeX

$$$$ \\operatorname{range}(\\mathrm{inclusion}\\, h) = \\{ x : t \\mid (x : \\alpha) ∈ s \\} $$$$

Lean4

@[simp]
theorem range_inclusion (h : s ⊆ t) : range (inclusion h) = {x : t | (x : α) ∈ s} :=
  by
  ext ⟨x, hx⟩
  simp
    -- When `f` is injective, see also `Equiv.ofInjective`.

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