eq_of_preimage_val_eq_of_subset — Mathlib

English

If B ⊆ A, C ⊆ A and A ∩ B = A ∩ C, then B = C.

Русский

Если B ⊆ A, C ⊆ A и A ∩ B = A ∩ C, тогда B = C.

LaTeX

$$$B \\subseteq A \\land C \\subseteq A \\land A \\cap B = A \\cap C \\implies B = C$$$

Lean4

theorem eq_of_preimage_val_eq_of_subset (hB : B ⊆ A) (hC : C ⊆ A) (h : A ↓∩ B = A ↓∩ C) : B = C :=
  by
  simp only [← inter_eq_right] at hB hC
  simp only [Subtype.preimage_val_eq_preimage_val_iff, hB, hC] at h
  exact h

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