isPreconnected_setOf_sOppSide — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isPreconnected_setOf_sOppSide (s : AffineSubspace ℝ P) (x : P) : IsPreconnected {y | s.SOppSide 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_sOppSide_bot]
    exact isPreconnected_empty
  · by_cases hx : x ∈ s
    · simp only [hx, SOppSide, not_true, false_and, and_false]
      exact isPreconnected_empty
    · exact (isConnected_setOf_sOppSide hx h).isPreconnected

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