keys_subset_keys_of_entries_subset_entries

English

If s1.entries ⊆ s2.entries, then s1.keys ⊆ s2.keys.

Русский

Если s1.entries ⊆ s2.entries, то s1.keys ⊆ s2.keys.

LaTeX

$$s_1.entries \subseteq s_2.entries \Rightarrow s_1.keys \subseteq s_2.keys$$

Lean4

theorem keys_subset_keys_of_entries_subset_entries {s₁ s₂ : AList β} (h : s₁.entries ⊆ s₂.entries) :
    s₁.keys ⊆ s₂.keys := by
  intro k hk
  letI : DecidableEq α := Classical.decEq α
  have := h (mem_lookup_iff.1 (Option.get_mem (lookup_isSome.2 hk)))
  rw [← mem_lookup_iff, Option.mem_def] at this
  rw [← mem_keys, ← lookup_isSome, this]
  exact Option.isSome_some

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