inter_left — Mathlib

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⟩)⟩⟩

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