le_iSup — Mathlib

English

For a poset with a Frame structure, if a is an atom, then a is below the supremum of a family f exactly when there exists an index i with a ≤ f(i).

Русский

Для позиции с каркасной структурой, если a — атом, то a ≤ ⨆ i f(i) эквивалентно существованию индекса i с a ≤ f(i).

LaTeX

$$$ \\mathrm{IsAtom}(a) \\rightarrow \\bigl( a \\le \\bigvee_{i} f(i) \\iff \\exists i,\\ a \\le f(i) \\bigr)$$$

Lean4

protected theorem le_iSup (ha : IsAtom a) : a ≤ iSup f ↔ ∃ i, a ≤ f i :=
  by
  refine ⟨?_, fun ⟨i, hi⟩ => le_trans hi (le_iSup _ _)⟩
  change (a ≤ ⨆ i, f i) → _
  refine fun h => of_not_not fun ha' => ?_
  push_neg at ha'
  have ha'' : Disjoint a (⨆ i, f i) :=
    disjoint_iSup_iff.2 fun i => fun x hxa hxf =>
      le_bot_iff.2 <|
        of_not_not fun hx =>
          have hxa : x < a := (le_iff_eq_or_lt.1 hxa).resolve_left (by rintro rfl; exact ha' _ hxf)
          hx (ha.2 _ hxa)
  obtain rfl := le_bot_iff.1 (ha'' le_rfl h)
  exact ha.1 rfl

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