le_sup_iff — Mathlib

English

If s is SupIndep and t ⊆ s, i ∈ s, f(i) ≠ ⊥, then f(i) ≤ t.sup f iff i ∈ t.

Русский

Если s SupIndep и t ⊆ s, i ∈ s, f(i) ≠ ⊥, тогда f(i) ≤ t.sup f эквивално i ∈ t.

LaTeX

$$$\\text{SupIndep}(s,f) \\land t \\subseteq s \\land i \\in s \\land (f(i) \\neq ⊥) \\Rightarrow (f(i) \\le t.sup f) \\iff i \\in t.$$$

Lean4

theorem le_sup_iff (hs : s.SupIndep f) (hts : t ⊆ s) (hi : i ∈ s) (hf : ∀ i, f i ≠ ⊥) : f i ≤ t.sup f ↔ i ∈ t :=
  by
  refine ⟨fun h => ?_, le_sup⟩
  by_contra hit
  exact hf i (disjoint_self.1 <| (hs hts hi hit).mono_right h)

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