mem_iff_forall_le_or_ge — Mathlib

English

a ∈ s iff for all b ∈ s, a ≤ b or b ≤ a.

Русский

a принадлежит s тогда и только тогда, когда для всех b ∈ s выполняется a ≤ b или b ≤ a.

LaTeX

$$$a ∈ s \\\\iff \\\\forall b, b ∈ s \\\\rightarrow a ≤ b \\\\lor b ≤ a$$$

Lean4

theorem mem_iff_forall_le_or_ge : a ∈ s ↔ ∀ ⦃b⦄, b ∈ s → a ≤ b ∨ b ≤ a :=
  ⟨fun ha b => s.le_or_le ha, fun hb =>
    of_not_not fun ha =>
      Set.ne_insert_of_notMem _ ‹_› <| s.maxChain.2 (s.chain_le.insert fun c hc _ => hb hc) <| Set.subset_insert _ _⟩

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