pathComponentIn_mono — Mathlib

English

If F ⊆ G, then pathComponentIn F x ⊆ pathComponentIn G x for any x.

Русский

Если F ⊆ G, то pathComponentIn F x ⊆ pathComponentIn G x для любого x.

LaTeX

$$$$(F \subseteq G) \Rightarrow (\operatorname{pathComponentIn} F x \subseteq \operatorname{pathComponentIn} G x).$$$$

Lean4

@[gcongr]
theorem pathComponentIn_mono {G : Set X} (h : F ⊆ G) : pathComponentIn F x ⊆ pathComponentIn G x := fun _ ⟨γ, hγ⟩ ↦
  ⟨γ, fun t ↦ h (hγ t)⟩

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