compl_compl_himp_distrib — Mathlib

English

(a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ.

Русский

(a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ.

LaTeX

$$$(a \Rightarrow b)^{\complement\complement} = a^{\complement\complement} \Rightarrow b^{\complement\complement}$$$

Lean4

theorem compl_compl_himp_distrib (a b : α) : (a ⇨ b)ᶜᶜ = aᶜᶜ ⇨ bᶜᶜ :=
  by
  apply le_antisymm
  · rw [le_himp_iff, ← compl_compl_inf_distrib]
    exact compl_anti (compl_anti himp_inf_le)
  · refine le_compl_comm.1 ((compl_anti compl_sup_le_himp).trans ?_)
    rw [compl_sup_distrib, le_compl_iff_disjoint_right, disjoint_right_comm, ← le_compl_iff_disjoint_right]
    exact inf_himp_le

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