inter' — Mathlib

English

As an instance, if s and t are OrdConnected, then s ∩ t is OrdConnected.

Русский

В виде инстанции: если s и t OrdConnected, то их пересечение s ∩ t тоже OrdConnected.

LaTeX

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

Lean4

instance inter' {s t : Set α} [OrdConnected s] [OrdConnected t] : OrdConnected (s ∩ t) :=
  OrdConnected.inter ‹_› ‹_›

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