Plain-language statement
Two well-formed maps are equal if they have the same find? for every key.
Exact Lean statement
public theorem find?_ext [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m₁ m₂ : Map α β}
(wf₁ : m₁.WellFormed)
(wf₂ : m₂.WellFormed)
(h : ∀ k, m₁.find? k = m₂.find? k) :
m₁ = m₂Formal artifact
Lean source
public theorem find?_ext [LT α] [DecidableLT α] [StrictLT α] [DecidableEq α] {m₁ m₂ : Map α β} (wf₁ : m₁.WellFormed) (wf₂ : m₂.WellFormed) (h : ∀ k, m₁.find? k = m₂.find? k) : m₁ = m₂:= by apply eq_iff_toList_equiv wf₁ wf₂ |>.mp constructor · intro ⟨k, v⟩ h₁ have h₂ := (in_list_iff_find?_some wf₁).mp h₁ rw [h] at h₂ exact (in_list_iff_find?_some wf₂).mpr h₂ · intro ⟨k, v⟩ h₁ have h₂ := (in_list_iff_find?_some wf₂).mp h₁ rw [← h] at h₂ exact (in_list_iff_find?_some wf₁).mpr h₂- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/Data/Map.lean:471-486
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Find? notmem keys
Cedar.Data.Map.find?_notmem_keys
Plain-language statement
Inverse of find?_mem_toList, except that this requires wf
Source project: Cedar Specification
Person-level attribution pending.
Find? some iff in values
Cedar.Data.Map.find?_some_iff_in_values
Plain-language statement
The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above
Source project: Cedar Specification
Person-level attribution pending.
In list iff find? some
Cedar.Data.Map.in_list_iff_find?_some
Plain-language statement
The mpr direction of this does not need the wf precondition and, in fact, is available separately as find?_mem_toList above
Source project: Cedar Specification
Person-level attribution pending.