range_mk — Mathlib

English

For a fixed b, the range of the map y ↦ (b,y) equals the set of total-space elements whose projection is b.

Русский

Для фиксированного b множество образов отображения y ↦ (b,y) совпадает с теми элементами общего пространства, проекция которых равна b.

LaTeX

$$$$\operatorname{range}(\big(\uparrow\big) : E(b) \to \text{TotalSpace } F E) = \pi F E^{-1}(\{b\}).$$$$

Lean4

@[simp]
theorem range_mk (b : B) : range ((↑) : E b → TotalSpace F E) = π F E ⁻¹' { b } :=
  by
  apply Subset.antisymm
  · rintro _ ⟨x, rfl⟩
    rfl
  · rintro ⟨_, x⟩ rfl
    exact ⟨x, rfl⟩

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