isBounded_pi — Mathlib

English

The pi-univ set is bounded if and only if either some S_i is empty or all S_i are bounded.

Русский

Множество pi-univ ограничено тогда, когда либо некоторый S_i пуст, либо все S_i ограничены.

LaTeX

$$$\\operatorname{IsBounded}(\\pi\\,\\text{univ}\\,S) \\iff (\\exists i, S_i = \\varnothing) \\lor \\forall i, \\operatorname{IsBounded}(S_i)$$$

Lean4

theorem isBounded_pi : IsBounded (pi univ S) ↔ (∃ i, S i = ∅) ∨ ∀ i, IsBounded (S i) :=
  by
  by_cases hne : ∃ i, S i = ∅
  · simp [hne, univ_pi_eq_empty_iff.2 hne]
  · simp only [hne, false_or]
    simp only [not_exists, ← nonempty_iff_ne_empty, ← univ_pi_nonempty_iff] at hne
    exact isBounded_pi_of_nonempty hne

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