inter — Mathlib

English

If two subsets s and t are OrdConnected, then their intersection s ∩ t is OrdConnected.

Русский

Если подмножества s и t являются OrdConnected, то их пересечение s ∩ t также OrdConnected.

LaTeX

$$$\operatorname{OrdConnected}(s) \land \operatorname{OrdConnected}(t) \Rightarrow \operatorname{OrdConnected}(s \cap t)$$$

Lean4

theorem inter {s t : Set α} (hs : OrdConnected s) (ht : OrdConnected t) : OrdConnected (s ∩ t) :=
  ⟨fun _ hx _ hy => subset_inter (hs.out hx.1 hy.1) (ht.out hx.2 hy.2)⟩

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