isSome_iff — Mathlib

English

For every I in WithBot(Box ι), I is defined (not bottom) if and only if the underlying set is nonempty.

Русский

Для каждого I ∈ WithBot(Box ι) выполняется: I определено (не ⊥) тогда и только тогда, когда соответствующее множество непусто.

LaTeX

$$$\forall I : WithBot(Box ι), I \neq \bot \iff (I : Set (ι \to \mathbb{R})) \neq \varnothing$$$

Lean4

theorem isSome_iff : ∀ {I : WithBot (Box ι)}, I.isSome ↔ (I : Set (ι → ℝ)).Nonempty
  | ⊥ => by
    unfold Option.isSome
    simp
  | (I : Box ι) => by
    unfold Option.isSome
    simp [I.nonempty_coe]

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