notMem_of_max_lt — Mathlib

English

In a linear order, if b < a and s.max equals some element, then a is not in s.

Русский

Во линейном порядке, если b < a и максимум множества s равен некоторому элементу, то a не принадлежит s.

LaTeX

$$Not (a ∈ s) given max constraints: a ∉ s when s.max = b.$$

Lean4

theorem notMem_of_max_lt {s : Finset α} {a b : α} (h₁ : b < a) (h₂ : s.max = ↑b) : a ∉ s :=
  Finset.notMem_of_max_lt_coe <| h₂.trans_lt <| WithBot.coe_lt_coe.mpr h₁

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