Proposition cha_frobenius {H : complete_heyting_algebra} {I : UU} (f : I → H) (x : H) : (x ∧ \/_{ i } f i) = \/_{ i } (x ∧ f i). Proof. use cha_le_antisymm. - rewrite (cha_min_comm x (\/_{ i } f i)). use cha_from_le_exp. use cha_lub_le. intro i. use cha_to_le_exp. rewrite (cha_min_comm (f i) x). exact (cha_le_lub_pt (λ j, x ∧ f j) i). - use cha_lub_le. intro i ; cbn. use cha_min_le_min_r. apply cha_le_lub_pt. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.BinaryOperations. Require Import UniMath.OrderTheory.Lattice.Lattice. Require Import UniMath.OrderTheory.Lattice.Bounded. Require Import UniMath.OrderTheory.Lattice.Heyting. Require Import UniMath.OrderTheory.Lattice.CompleteHeyting.