himp_bihimp — Mathlib

English

The implication of a to bihimp(b,c) equals the infimum of two implications: himp(a ∧ c, b) and himp(a ∧ b, c).

Русский

Импликация от a к bihimp(b,c) равна наименьшему из импликаций a ∧ c → b и a ∧ b → c.

LaTeX

$$$\operatorname{himp}(a, \operatorname{bihimp}(b,c)) = \min\big( \operatorname{himp}(a \wedge c, b), \operatorname{himp}(a \wedge b, c) \big)$$$

Lean4

theorem himp_bihimp : a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c) := by rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]

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