finite_option — Mathlib

English

A set of options over α is finite if and only if the set of α-values appearing as some is finite.

Русский

Множество значений типа Option α конечо тогда и только тогда, когда множество элементов α, встречающихся как some x, конечно.

LaTeX

$$$ (s : Set (Option α)).Finite \\iff {x : α | some x ∈ s}.Finite $$$

Lean4

theorem finite_option {s : Set (Option α)} : s.Finite ↔ {x : α | some x ∈ s}.Finite :=
  ⟨fun h => h.preimage_embedding Embedding.some, fun h =>
    ((h.image some).insert none).subset fun x =>
      x.casesOn (fun _ => Or.inl rfl) fun _ hx => Or.inr <| mem_image_of_mem _ hx⟩

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