fintypeOfMemBounds — Mathlib

English

A set with lower and upper bounds in a locally finite order carries a finite type structure.

Русский

Множество, ограниченное снизу и сверху в локально конечном порядке, обладает конечной структурой типа.

LaTeX

$$$ \forall s \subseteq \alpha,\; (a \in lowerBounds(s)) \land (b \in upperBounds(s)) \Rightarrow Fintype\,s $$$

Lean4

/-- A set with upper and lower bounds in a locally finite order is a fintype -/
def _root_.Set.fintypeOfMemBounds {s : Set α} [DecidablePred (· ∈ s)] (ha : a ∈ lowerBounds s)
    (hb : b ∈ upperBounds s) : Fintype s :=
  Set.fintypeSubset (Set.Icc a b) fun _ hx => ⟨ha hx, hb hx⟩

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