exists_subtype_range_iff — Mathlib

English

(∃ a : range f, p a) ↔ ∃ i, p ⟨f i, mem_range_self i⟩.

Русский

Существование элемента a в диапазоне f как элемента типа range f эквивалентно существованию i, для которого верно p(⟨f i, mem_range_self i⟩).

LaTeX

$$$ ( \\exists a : \\operatorname{range} f,\ p(a)) \\;\\Leftrightarrow\\; \\exists i\\, p\\big(\\langle f(i), \\operatorname{mem\\_range\\_self}(i) \\rangle\\big).$$$

Lean4

theorem exists_subtype_range_iff {p : range f → Prop} : (∃ a : range f, p a) ↔ ∃ i, p ⟨f i, mem_range_self _⟩ := by
  grind

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