refl

Mathlib.Topology.Connected.PathConnected

URI: https://scilib.ai/kg/mathlib#JoinedIn.refl

English

If x ∈ F, then there is a trivial constant path in F from x to x, so JoinedIn F x x holds.

Русский

Если x ∈ F, то существует тривиальный константный путь в F от x к x, следовательно JoinedIn F x x.

LaTeX

$$JoinedIn F x x$$

Lean4

theorem refl (h : x ∈ F) : JoinedIn F x x :=
  ⟨Path.refl x, fun _t => h⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru