eq_of_mem_ordConnectedSection_of_uIcc_subset

English

If x, y ∈ s.ordConnectedSection and [[x, y]] ⊆ s, then x = y.

Русский

Если x, y ∈ s.ordConnectedSection и [[x, y]] ⊆ s, тогда x = y.

LaTeX

$$$x \in \operatorname{ordConnectedSection}(s) \land y \in \operatorname{ordConnectedSection}(s) \land [[x, y]] \subseteq s \Rightarrow x = y$$$

Lean4

theorem eq_of_mem_ordConnectedSection_of_uIcc_subset (hx : x ∈ ordConnectedSection s) (hy : y ∈ ordConnectedSection s)
    (h : [[x, y]] ⊆ s) : x = y := by
  rcases hx with ⟨x, rfl⟩; rcases hy with ⟨y, rfl⟩
  exact
    ordConnectedProj_eq.2
      (mem_ordConnectedComponent_trans
        (mem_ordConnectedComponent_trans (ordConnectedProj_mem_ordConnectedComponent _ _) h)
        (mem_ordConnectedComponent_ordConnectedProj _ _))

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