map_himp_le — Mathlib

English

A generalized implication operation HImp is defined on nuclei, generalizing Heyting algebra implication.

Русский

Определён обобщённый операция импликации HImp на нуклеусах, обобщая импликацию в Heyting-алгебре.

LaTeX

$$$\text{HImp}(m,n)$ is a nucleus-valued implication$$

Lean4

theorem map_himp_le : n (x ⇨ y) ≤ x ⇨ n y := by
  rw [le_himp_iff]
  calc
    n (x ⇨ y) ⊓ x
    _ ≤ n (x ⇨ y) ⊓ n x := by gcongr; exact n.le_apply
    _ = n (y ⊓ x) := by rw [← map_inf, himp_inf_self]
    _ ≤ n y := by gcongr; exact inf_le_left

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