iInf_gt_eq_self — Mathlib

English

For any a in ENNReal, the infimum over b of the set of all b with a < b equals a. In symbols, iInf b, a < b = a.

Русский

Для любого a ∈ ENNReal: iInf(b, b>a) = a.

LaTeX

$$$ \forall a:\ iInf_{b} \bigl( a < b \bigr) \; = \; a $$$

Lean4

@[simp]
theorem iInf_gt_eq_self (a : ℝ≥0∞) : ⨅ b, ⨅ _ : a < b, b = a :=
  by
  refine le_antisymm ?_ (le_iInf₂ fun b hb ↦ hb.le)
  refine le_of_forall_gt fun c hac ↦ ?_
  obtain ⟨d, had, hdc⟩ := exists_between hac
  exact (iInf₂_le_of_le d had le_rfl).trans_lt hdc

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