subset_ordConnectedComponent — Mathlib

English

If s ⊆ t and x ∈ s with s OrdConnected, then s ⊆ ordConnectedComponent(t,x).

Русский

Если s ⊆ t и x ∈ s, и s упорядоченно связано, то s ⊆ ordConnectedComponent(t,x).

LaTeX

$$$s \\subseteq t \\Rightarrow x \\in s \\Rightarrow s \\subseteq \\operatorname{ordConnectedComponent}(t,x)$$$

Lean4

theorem subset_ordConnectedComponent {t} [h : OrdConnected s] (hs : x ∈ s) (ht : s ⊆ t) :
    s ⊆ ordConnectedComponent t x := fun _ hy => (h.uIcc_subset hs hy).trans ht

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