instHImp — Mathlib

English

There is a noncomputable instance of a logical implication on the subtype: hImp x y = ⟨x ⇨ y, x.prop.himp y.prop⟩.

Русский

Существует невычисляемый инстанс логической импликации над подтипом: hImp x y = ⟨x ⇨ y, x.prop.himp y.prop⟩.

LaTeX

$$$$\\text{HImp}(x,y) = \\langle x \\Rightarrow y, x.prop.himp y.prop \\rangle.$$$$

Lean4

noncomputable instance instHImp : HImp (Subtype (MeasurableSet : Set α → Prop)) where
  himp x y := ⟨x ⇨ y, x.prop.himp y.prop⟩

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