ordConnectedProj_eq — Mathlib

English

For x, y ∈ s, ordConnectedProj(s)(x) = ordConnectedProj(s)(y) if and only if [[(x : α), y]] ⊆ s.

Русский

Для x, y ∈ s, ordConnectedProj(s)(x) = ordConnectedProj(s)(y) тогда и только тогда, когда [[(x : α), y]] ⊆ s.

LaTeX

$$$\operatorname{ordConnectedProj}(s, x) = \operatorname{ordConnectedProj}(s, y) \iff [[(x : \alpha), y]] \subseteq s$$$

Lean4

@[simp]
theorem ordConnectedProj_eq {x y : s} : ordConnectedProj s x = ordConnectedProj s y ↔ [[(x : α), y]] ⊆ s :=
  by
  constructor <;> intro h
  · rw [← mem_ordConnectedComponent, ← ordConnectedComponent_ordConnectedProj, h,
      ordConnectedComponent_ordConnectedProj, self_mem_ordConnectedComponent]
    exact y.2
  · simp only [ordConnectedProj, ordConnectedComponent_eq h]

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