pathComponentIn_nonempty_iff — Mathlib

English

The path component in F of x is nonempty exactly when x ∈ F.

Русский

Компонента пути x в F непустая тогда и только тогда, когда x ∈ F.

LaTeX

$$$$(\operatorname{pathComponentIn} F x) \text{ Nonempty } \iff x \in F.$$$$

Lean4

theorem pathComponentIn_nonempty_iff : (pathComponentIn F x).Nonempty ↔ x ∈ F :=
  ⟨fun ⟨_, ⟨γ, hγ⟩⟩ ↦ γ.source ▸ hγ 0, fun hx ↦ ⟨x, mem_pathComponentIn_self hx⟩⟩

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