English
If A is exposed to C and C ⊆ B, then A ∩ B is exposed to C.
Русский
Если A экспонировано относительно C и C ⊆ B, то A ∩ B экспонировано относительно C.
LaTeX
$$$$ (IsExposed\ 𝕜\ A\ C) \to (C \subseteq B) \to IsExposed\ 𝕜\ (A \cap B)\ C. $$$$
Lean4
theorem inter_left (hC : IsExposed 𝕜 A C) (hCB : C ⊆ B) : IsExposed 𝕜 (A ∩ B) C :=
by
rintro ⟨w, hw⟩
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩
exact
⟨l,
Subset.antisymm (fun x hx => ⟨⟨hx.1, hCB hx⟩, fun y hy => hx.2 y hy.1⟩) fun x ⟨⟨hxC, _⟩, hx⟩ =>
⟨hxC, fun y hy => (hw.2 y hy).trans (hx w ⟨hC.subset hw, hCB hw⟩)⟩⟩