English
Let α be a type with a notion of greatest lower bounds for sets. If p and q are propositions, f1 : p → α, f2 : q → α, and p ↔ q, and if f1 (pq.mpr x) = f2 x for all x, then the infimum of f1 equals the infimum of f2.
Русский
Пусть α — тип с существованием наибольших нижних границ множеств. Пусть p и q — пропозиции, f1 : p → α, f2 : q → α, и p ↔ q, и если f1 (pq.mpr x) = f2 x для всех x, то наибольшие нижние границы функций f1 и f2 равны.
LaTeX
$$$ (p \leftrightarrow q) \land (\forall x, f_1(pq.mpr x) = f_2 x) \Rightarrow \iInf f_1 = \iInf f_2 $$$
Lean4
@[congr]
theorem iInf_congr_Prop {p q : Prop} {f₁ : p → α} {f₂ : q → α} (pq : p ↔ q) (f : ∀ x, f₁ (pq.mpr x) = f₂ x) :
iInf f₁ = iInf f₂ :=
@iSup_congr_Prop αᵒᵈ _ p q f₁ f₂ pq f
