English
For finite s,t ⊆ α in a distributive lattice, the power set of their intersection equals the infimum of their powersets: (s ∩ t).powerset = s.powerset ⊼ t.powerset.
Русский
Для конечных s, t ⊆ α в распределительной решётке выполняется: (s ∩ t).powerset = s.powerset ⊼ t.powerset.
LaTeX
$$$ (s \cap t).powerset = s.powerset \wedge t.powerset $$$
Lean4
@[simp]
theorem powerset_inter (s t : Finset α) : (s ∩ t).powerset = s.powerset ⊼ t.powerset :=
by
ext u
simp only [mem_infs, mem_powerset, inf_eq_inter]
refine ⟨fun h ↦ ⟨_, inter_subset_left (s₂ := u), _, inter_subset_left (s₂ := u), ?_⟩, ?_⟩
· rwa [← inter_inter_distrib_right, inter_eq_right]
· rintro ⟨v, hv, w, hw, rfl⟩
exact inter_subset_inter hv hw
