notMem_of_lt_min — Mathlib

English

Let S be a finite nonempty subset of a linearly ordered set A. If a < b and the minimum of S equals b, then a ∉ S.

Русский

Пусть S — конечное непустое подмножество линейно упорядоченного множества A. Если a < b и минимум S равен b, то a не принадлежит S.

LaTeX

$$$$\forall S \subseteq A,\ S \text{ finite nonempty},\ \forall a,b \in A,\ a < b \land \min S = b \Rightarrow a \notin S.$$$$

Lean4

theorem notMem_of_lt_min {s : Finset α} {a b : α} (h₁ : a < b) (h₂ : s.min = ↑b) : a ∉ s :=
  Finset.notMem_of_coe_lt_min <| (WithTop.coe_lt_coe.mpr h₁).trans_eq h₂.symm

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