restrict — Mathlib

English

Let S be an order-connected subset of a linearly ordered set, and let t be any subset. Then the set defined by restricting the membership predicate to S along t is again order-connected.

Русский

Пусть S — множество, связное по порядку, внутри линейно упорядоченного множества; пусть t — любое множество. Тогда множество {x | ограничение по t от принадлежности x к S} также является связанным по порядку.

LaTeX

$$$\\operatorname{OrdConnected}({x \\mid \\text{restrict } t (\\cdot \\in s)\\,x})$ given $s$ is $\\operatorname{OrdConnected}$.$$

Lean4

protected theorem restrict (hs : s.OrdConnected) : {x | restrict t (· ∈ s) x}.OrdConnected :=
  ⟨fun _ hx _ hy _ hz => hs.out hx hy hz⟩

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