ordConnectedComponent_inter — Mathlib

English

The order-connected component of the intersection of two sets equals the intersection of their order-connected components: ordConnectedComponent(s ∩ t, x) = ordConnectedComponent(s, x) ∩ ordConnectedComponent(t, x).

Русский

ordConnectedComponent(s ∩ t, x) = ordConnectedComponent(s, x) ∩ ordConnectedComponent(t, x).

LaTeX

$$$\operatorname{ordConnectedComponent}(s \cap t, x) = \operatorname{ordConnectedComponent}(s, x) \cap \operatorname{ordConnectedComponent}(t, x)$$$

Lean4

theorem ordConnectedComponent_inter (s t : Set α) (x : α) :
    ordConnectedComponent (s ∩ t) x = ordConnectedComponent s x ∩ ordConnectedComponent t x := by
  simp [ordConnectedComponent, setOf_and]

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