subsingleton_cod — Mathlib

English

If every fiber β(a) is Subsingleton, then the entire function-like type F is Subsingleton.

Русский

Если каждый карман (β(a)) является подмножество, то вся типовая конструкция F также является одиночной (subsingleton).

LaTeX

$$$\big(\forall a, \operatorname{Subsingleton}(\beta(a))\big) \Rightarrow \operatorname{Subsingleton}(F).$$$

Lean4

/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search. -/
theorem subsingleton_cod [∀ a, Subsingleton (β a)] : Subsingleton F :=
  coe_injective.subsingleton

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