English
The type of functions f : ∀ a, β a with ∀ a, p a (f a) is equivalent to the type ∀ a, { b : β a // p a b }.
Русский
Тип функций f : ∀ a, β a с условием ∀ a, p a (f a) эквивалентен типу ∀ a, { b : β a // p a b }.
LaTeX
$$$\\{ f : \\forall a, \\beta a \\; // \\forall a, p a (f a) \\} \\simeq \\forall a, \\{ b : \\beta a // p a b \\}$$$
Lean4
/-- The type of functions `f : ∀ a, β a` such that for all `a` we have `p a (f a)` is equivalent
to the type of functions `∀ a, {b : β a // p a b}`. -/
def subtypePiEquivPi {β : α → Sort v} {p : ∀ a, β a → Prop} :
{ f : ∀ a, β a // ∀ a, p a (f a) } ≃ ∀ a, { b : β a // p a b }
where
toFun := fun f a => ⟨f.1 a, f.2 a⟩
invFun := fun f => ⟨fun a => (f a).1, fun a => (f a).2⟩
left_inv := by
rintro ⟨f, h⟩
rfl
right_inv := by
rintro f
funext a
exact Subtype.ext rfl
