joinedIn

Mathlib.Topology.Connected.PathConnected

URI: https://scilib.ai/kg/mathlib#Inseparable.joinedIn

English

If x and y are inseparable and x,y ∈ F, then there exists a path in F from x to y.

Русский

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

LaTeX

$$Inseparable x y → x ∈ F → y ∈ F → JoinedIn F x y$$

Lean4

theorem joinedIn (h : Inseparable x y) (hx : x ∈ F) (hy : y ∈ F) : JoinedIn F x y :=
  h.specializes.joinedIn hx hy

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

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

Разделы

Аффилиация

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