English
If both B and C are exposed subsets of A, then their intersection B ∩ C is also exposed with respect to A.
Русский
Если B и C — экспонированные подмножества A, то их пересечение B ∩ C тоже экспонировано относительно A.
LaTeX
$$$$ (IsExposed\ 𝕜\ A\ B) \to (IsExposed\ 𝕜\ A\ C) \to IsExposed\ 𝕜\ A\ (B \cap C). $$$$
Lean4
protected theorem inter [IsOrderedRing 𝕜] [ContinuousAdd 𝕜] {A B C : Set E} (hB : IsExposed 𝕜 A B)
(hC : IsExposed 𝕜 A C) : IsExposed 𝕜 A (B ∩ C) :=
by
rintro ⟨w, hwB, hwC⟩
obtain ⟨l₁, rfl⟩ := hB ⟨w, hwB⟩
obtain ⟨l₂, rfl⟩ := hC ⟨w, hwC⟩
refine ⟨l₁ + l₂, Subset.antisymm ?_ ?_⟩
· rintro x ⟨⟨hxA, hxB⟩, ⟨-, hxC⟩⟩
exact ⟨hxA, fun z hz => add_le_add (hxB z hz) (hxC z hz)⟩
rintro x ⟨hxA, hx⟩
refine ⟨⟨hxA, fun y hy => ?_⟩, hxA, fun y hy => ?_⟩
· exact (add_le_add_iff_right (l₂ x)).1 ((add_le_add (hwB.2 y hy) (hwC.2 x hxA)).trans (hx w hwB.1))
· exact (add_le_add_iff_left (l₁ x)).1 (le_trans (add_le_add (hwB.2 x hxA) (hwC.2 y hy)) (hx w hwB.1))
