preimage_coe — Mathlib

English

If W ⊆ X is path-connected and W ⊆ U, then viewed as a subset of U, W is path-connected.

Русский

Если W ⊆ X путево связно и W ⊆ U, то W как подмножество U также путево связано.

LaTeX

$$IsPathConnected(((\uparrow) : U → X)^{-1}' W)$$

Lean4

/-- If a set `W` is path-connected, then it is also path-connected when seen as a set in a smaller
ambient type `U` (when `U` contains `W`). -/
theorem preimage_coe {U W : Set X} (hW : IsPathConnected W) (hWU : W ⊆ U) : IsPathConnected (((↑) : U → X) ⁻¹' W) := by
  rwa [IsInducing.subtypeVal.isPathConnected_iff, Subtype.image_preimage_val, inter_eq_right.2 hWU]

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