isPreconnected_setOf_wOppSide — Mathlib

English

Let s be an affine subspace and x ∈ P. Then {y | s.WOppSide x y} is preconnected.

Русский

Пусть s — аффинное подпространство и x ∈ P. Тогда {y | s.WOppSide x y} предсвязано.

LaTeX

$$$\text{IsPreconnected}\bigl\{y \mid s.WOppSide(x,y)\bigr\}.$$$

Lean4

theorem isPreconnected_setOf_wOppSide (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.WOppSide x y} :=
  by
  rcases Set.eq_empty_or_nonempty (s : Set P) with (h | h)
  · rw [coe_eq_bot_iff] at h
    simp only [h, not_wOppSide_bot]
    exact isPreconnected_empty
  · exact (isConnected_setOf_wOppSide x h).isPreconnected

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