forall_subtype_range_iff — Mathlib

English

Let f: ι → α and p: range f → Prop. Then p holds for all a ∈ range f iff p holds on every canonical image ⟨f i, mem_range_self i⟩.

Русский

Пусть f: ι → α и p: range f → Prop. Тогда p применяется ко всем элементам диапазона f тогда и только тогда, когда p выполняется для каждого канонического элемента ⟨f(i), mem_range_self(i)⟩.

LaTeX

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

Lean4

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

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